Proving termination with multiset orderings

Cited in

(only showing first 100 items - show all)

A complexity tradeoff in ranking-function termination proofs
Giles's game and the proof theory of Łukasiewicz logic
Differential dynamic logic for hybrid systems
Context unification with one context variable
Termination orderings for associative-commutative rewriting systems
A theory for nondeterminism, parallelism, communication, and concurrency
Constructing recursion operators in intuitionistic type theory
Termination of rewriting
Path of subterms ordering and recursive decomposition ordering revisited
The Church-Rosser property for ground term-rewriting systems is decidable
History and basic features of the critical-pair/completion procedure
Extension functions for multiset orderings
Only prime superpositions need be considered in the Knuth-Bendix completion procedure
Critical pair criteria for completion
On termination of the direct sum of term-rewriting systems
A geometrical approach to multiset orderings
Equational problems and disunification
A note on simplification orderings
Definability in dynamic logic
On multiset orderings
Posets admitting a unique order-compatible topology
What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
Combining matching algorithms: The regular case
A general criterion for avoiding infinite unfolding during partial deduction
Conditional narrowing modulo a set of equations
Completion for rewriting modulo a congruence
Superposition theorem proving for abelian groups represented as integer modules
Decidability of behavioural equivalence in unary PCF
Self-stabilizing extensions for message-passing systems
Modularity of confluence: A simplified proof
Confluence by decreasing diagrams
A derived algorithm for evaluating -expressions over abstract sets
Completeness results for basic narrowing
The translation power of top-down tree-to-graph transducers
On proving the termination of algorithms by machine
On the modularity of termination of term rewriting systems
Buchberger's algorithm: The term rewriter's point of view
Simple termination of rewrite systems
Deciding the word problem in the union of equational theories.
A uniform framework for term and graph rewriting applied to combined systems
Uniform interpolation and sequent calculi in modal logic
Skolemization and Herbrand theorems for lattice-valued logics
On the computational strength of pure ambient calculi
Partial orderings for sets of multisets
Proof of termination of the rewriting system SUBSET on CCL
Equality between functionals in the presence of coproducts
On terminating lemma speculations.
Right-linear half-monadic term rewrite systems
Three-variable statements of set-pairing
Deciding confluence of certain term rewriting systems in polynomial time
Intersection types for explicit substitutions
A linear time algorithm for monadic querying of indefinite data over linearly ordered domains
Decidability of bounded second order unification
Total termination of term rewriting
Infinite complete group presentations
Linear and unit-resulting refutations for Horn theories
An improved general path order
Jumping and escaping: modular termination and the abstract path ordering
Superposition decides the first-order logic fragment over ground theories
Sequent calculi for intuitionistic Gödel-Löb logic
A general framework for Noetherian well ordered polynomial reductions
Variadic equational matching in associative and commutative theories
Set of support, demodulation, paramodulation: a historical perspective
Ground joinability and connectedness in the superposition calculus
A framework for approximate generalization in quantitative theories
The G4i analogue of a G3i sequent calculus
AC simplifications and closure redundancies in the superposition calculus
Weighted models for higher-order computation
Uniform interpolation and the existence of sequent calculi
Formally verified tableau-based reasoners for a description logic
Ensuring termination by typability
Reduction relations for monoid semirings
Type-theoretic approaches to ordinals
A semantic account of strong normalization in linear logic
Proof theory for lattice-ordered groups
Contextual equivalence for inductive definitions with binders in higher order typed functional programming
A Completion Method to Decide Reachability in Rewrite Systems
A Lambda-Free Higher-Order Recursive Path Order
Decision Procedures for Automating Termination Proofs
Mobile Processes and Termination
The ideal approach to computing closed subsets in well-quasi-orderings
Implementing term rewriting by jungle evaluation
Labelled Calculi for Łukasiewicz Logics
Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
Paramodulation with non-monotonic orderings and simplification
scientific article; zbMATH DE number 3926235 (Why is no real title available?)
On unification and admissible rules in Gabbay-de Jongh logics
On an interpretation of second order quantification in first order intuitionistic propositional logic
Contraction-free sequent calculi for intuitionistic logic
Intermutation
The order types of termination orderings on monadic terms, strings and multisets
On deciding satisfiability by theorem proving with speculative inferences
Proof pearl: a formal proof of Higman's lemma in ACL2
Size-based termination of higher-order rewriting
scientific article; zbMATH DE number 6841178 (Why is no real title available?)
Checking admissibility using natural dualities
Termination of theorem proving by reuse
Extensions of arithmetic for proving termination of computations
SOME EXACT SEQUENCES FOR THE HOMOTOPY (BI-)MODULE OF A MONOID
A multi-dimensional terminological knowledge representation language

This page was built for publication: Proving termination with multiset orderings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3868730)