Refutational theorem proving for hierarchic first-order theories

DOI10.1007/BF01190829zbMath0797.03008MaRDI QIDQ1328182

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Publication date: 4 July 1994

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

zbMATH Keywords

quantifier eliminationsuperpositionresolutionconstraintsalgebraic specificationterm rewritingvariable abstractionconstraint refutationhierarchic first-order theories

Mathematics Subject Classification ID

Related Items (36)

A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Symbol elimination and applications to parametric entailment problems ⋮ Superposition Modulo Non-linear Arithmetic ⋮ Beagle – A Hierarchic Superposition Theorem Prover ⋮ On First-Order Model-Based Reasoning ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ An Extension of the Knuth-Bendix Ordering with LPO-Like Properties ⋮ The Ackermann approach for modal logic, correspondence theory and second-order reduction ⋮ Model evolution with equality -- revised and implemented ⋮ Modular proof systems for partial functions with Evans equality ⋮ Superposition as a decision procedure for timed automata ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ A combined superposition and model evolution calculus ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Making theory reasoning simpler ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ Superposition for Bounded Domains ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ First-Order Resolution Methods for Modal Logics ⋮ A superposition calculus for abductive reasoning ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ A comprehensive framework for saturation theorem proving ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Combining induction and saturation-based theorem proving ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Model completeness, covers and superposition ⋮ On invariant synthesis for parametric systems ⋮ A complete and terminating approach to linear integer solving ⋮ Superposition Modulo Linear Arithmetic SUP(LA) ⋮ A comprehensive framework for saturation theorem proving ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I

Cites Work

• Efficient deduction in equality Horn logic by Horn-completion
• A resolution principle for a logic with restricted quantifiers
• Automated deduction by theory resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Refutational theorem proving for hierarchic first-order theories