Search
Search Results
-
Admissible Ordering on Monomials is Well-Founded: A Constructive Proof
AbstractIn this paper, we consider a constructive proof of the termination of the normal form (NF) algorithm for multivariate polynomials, as well as...
-
Well-Founded Unions
Given two or more well-founded (terminating) binary relations, when can one be sure that their union is likewise well-founded? We suggest new...
-
Higher-Order LCTRSs and Their Termination
Logically constrained term rewriting systems (LCTRSs) are a formalism for program analysis with support for data types that are not (co)inductively...
-
Set of Support, Demodulation, Paramodulation: A Historical Perspective
This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR founder Lawrence T. (Larry) Wos. Larry’s main technical...
-
Fixed Points and Noetherian Topologies
Noetherian spaces are a generalisation of well-quasi-orderings to topologies, that can be used to prove termination of programs. They find...
-
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover
The main topic of this article are SGGS decision procedures for fragments of first-order logic without equality. SGGS ( Semantically-Guided...
-
Resilience and Home-Space for WSTS
Resilience of unperfect systems is a key property for improving safety by insuring that if a system could go into a bad state in...
-
Tuple Interpretations for Termination of Term Rewriting
Interpretation methods constitute a foundation of the termination analysis of term rewriting. From time to time, remarkable instances of...
-
Product-form estimators: exploiting independence to scale up Monte Carlo
We introduce a class of Monte Carlo estimators that aim to overcome the rapid growth of variance with dimension often observed for standard...
-
A Comprehensive Framework for Saturation Theorem Proving
A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only...
-
Cellular structure of the Pommaret-Seiler resolution for quasi-stable ideals
We prove that the Pommaret-Seiler resolution for quasi-stable ideals is cellular and give a cellular structure for it. This shows that this...
-
Branch-Well-Structured Transition Systems and Extensions
We propose a relaxation to the definition of a well-structured transition systems (WSTS) while retaining the decidability of boundedness and...
-
Self-Organizing Multi-User UAV Swarm Simulation Platform
AbstractUnmanned aerial vehicles (UAV) swarms offer a cost-effective, time-efficient data collection and analysis solution across various...
-
Scientific eminence and scientific hierarchy: bibliometric prediction of fellowship in the Australian Academy of Science
Research metrics are known to predict many markers of scientific eminence, but fellowship in learned academies has not been examined in this context....
-
Confluence of Terminating Rewriting Computations
Rewriting is an intentional model of computation which is inherently non-deterministic. Defining functions by rewriting requires to prove that the...
-
A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
There have been some important methods of combining a recursive path ordering and Tait-Girard’s computability argument to provide an ordering for...
-
Artificial intelligence-related anomies and predictive policing: normative (dis)orders in liberal democracies
This article links three rarely considered dimensions related to the implementation of artificial intelligence (AI)-based technologies in the form of...
-
Term Orderings for Non-reachability of (Conditional) Rewriting
We propose generalizations of reduction pairs, well-established techniques for proving termination of term rewriting, in order to prove...
-
Multi-Dimensional Interpretations for Termination of Term Rewriting
Interpretation methods constitute a foundation of termination analysis for term rewriting. From time to time remarkable instances of interpretation...
-
Lung cancer survival prognosis using a two-stage modeling approach
Lung cancer, the second most prevalent form of cancer with the highest mortality rate, necessitates the stratification of patients based on their...
