Proving termination with multiset orderings

Cited in

(only showing first 100 items - show all)

A completion procedure for conditional equations
Using forcing to prove completeness of resolution and paramodulation
Reduction relations for monoid semirings
On termination of the direct sum of term-rewriting systems
On terminating lemma speculations.
Type-theoretic approaches to ordinals
Complete axiomatizations of some quotient term algebras
On weakly confluent monadic string-rewriting systems
Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
Term rewriting induction
On an interpretation of second order quantification in first order intuitionistic propositional logic
Total termination of term rewriting
Modularity of confluence: A simplified proof
Set of support, demodulation, paramodulation: a historical perspective
A framework for approximate generalization in quantitative theories
The G4i analogue of a G3i sequent calculus
Simple termination of rewrite systems
On the modularity of termination of term rewriting systems
AC simplifications and closure redundancies in the superposition calculus
Total termination of term rewriting
Partial orderings for sets of multisets
On unification and admissible rules in Gabbay-de Jongh logics
Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
Proof transformation for non-compatible rewriting
A general criterion for avoiding infinite unfolding during partial deduction
Skolemization and Herbrand theorems for lattice-valued logics
Completion for rewriting modulo a congruence
A semantic account of strong normalization in linear logic
Infinite complete group presentations
Complete equational unification based on an extension of the Knuth-Bendix completion procedure
Normal forms for fuzzy logics: a proof-theoretic approach
Path of subterms ordering and recursive decomposition ordering revisited
Canonical ground Horn theories
The order types of termination orderings on monadic terms, strings and multisets
Rippling: A heuristic for guiding inductive proofs
On some homotopical and homological properties of monoid presentations.
Intermutation
Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem
Reachability in Petri nets with inhibitor arcs
Decision Procedures for Automating Termination Proofs
Conditional narrowing modulo a set of equations
Differential dynamic logic for hybrid systems
Left-linear completion with AC axioms
Orderings for term-rewriting systems
A maximal-literal unit strategy for horn clauses
Labelled Calculi for Łukasiewicz Logics
Mobile Processes and Termination
Posets admitting a unique order-compatible topology
Deleting string rewriting systems preserve regularity
Mechanised uniform interpolation for modal logics K, GL, and iSL
Equality between functionals in the presence of coproducts
An improved general path order
What's so special about Kruskal's theorem and the ordinal $\Gamma{}_ 0$? A survey of some results in proof theory
Three-variable statements of set-pairing
A linear time algorithm for monadic querying of indefinite data over linearly ordered domains
Decidability of behavioural equivalence in unary PCF
Proof theory for lattice-ordered groups
Buchberger's algorithm: The term rewriter's point of view
Lazy narrowing: strong completeness and eager variable elimination (extended abstract)
Contraction-free sequent calculi for intuitionistic logic
scientific article; zbMATH DE number 6841178 (Why is no real title available?)
Self-stabilizing extensions for message-passing systems
Proof pearl: a formal proof of Higman's lemma in ACL2
A SAT-Based Approach to Size Change Termination with Global Ranking Functions
On deciding satisfiability by theorem proving with speculative inferences
A theory for nondeterminism, parallelism, communication, and concurrency
scientific article; zbMATH DE number 7204430 (Why is no real title available?)
Towards a foundation of completion procedures as semidecision procedures
Size-based termination of higher-order rewriting
Superposition theorem proving for abelian groups represented as integer modules
Completeness results for basic narrowing
Right-linear half-monadic term rewrite systems
Unification in a combination of arbitrary disjoint equational theories
A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems
A complexity tradeoff in ranking-function termination proofs
A generic deskolemization strategy
Termination Analysis of CHR Revisited
Reasoning about vectors: satisfiability modulo a theory of sequences
Variadic equational matching in associative and commutative theories
A saturation-based unification algorithm for higher-order rational patterns
Decidability of bounded second order unification
Uniform interpolation and the existence of sequent calculi
Leanest quasi-orderings
A descriptive type foundation for RDF Schema
Proof normalization for resolution and paramodulation
Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications
Reducibility constraints in superposition
scientific article; zbMATH DE number 7471678 (Why is no real title available?)
Termination of rewriting
Combining matching algorithms: The regular case
Definability in dynamic logic
On the computational strength of pure ambient calculi
Rewriting techniques for program synthesis
Random ordering of semiprimes
Deciding confluence of certain term rewriting systems in polynomial time
Proof theory for Lax Logic
Confluence by decreasing diagrams
Termination orderings for associative-commutative rewriting systems
On proving the termination of algorithms by machine
Linearizing well quasi-orders and bounding the length of bad sequences

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)