Ordered chaining calculi for first-order theories of transitive relations

DOI10.1145/293347.293352zbMath1065.68615OpenAlexW2027752737MaRDI QIDQ3158528

Leo Bachmair, Harald Ganzinger

Publication date: 25 January 2005

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/293347.293352

Mathematics Subject Classification ID

Related Items (23)

Automated theorem proving by resolution in non-classical logics ⋮ Proof theory for locally finite many-valued logics: semi-projective logics ⋮ On First-Order Model-Based Reasoning ⋮ A first polynomial non-clausal class in many-valued logic ⋮ Modular proof systems for partial functions with Evans equality ⋮ Deciding expressive description logics in the framework of resolution ⋮ On Automating the Calculus of Relations ⋮ Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators ⋮ Cyclic connections ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ On the Saturation of YAGO ⋮ An Extension of Complex Role Inclusion Axioms in the Description Logic $\mathcal{SROIQ}$ ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Ordered chaining for total orderings ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ A Generalisation of the Hyperresolution Principle to First Order Gödel Logic ⋮ Handling transitive relations in first-order automated reasoning ⋮ Automated verification of refinement laws ⋮ On the refutational completeness of signed binary resolution and hyperresolution ⋮ Hyperresolution for Gödel logic with truth constants ⋮ Layered clause selection for theory reasoning (short paper)

Uses Software

• PVS

This page was built for publication: Ordered chaining calculi for first-order theories of transitive relations