Rewrite-based Equational Theorem Proving with Selection and Simplification
From MaRDI portal
Publication:4304492
DOI10.1093/logcom/4.3.217zbMath0814.68117OpenAlexW2037085273MaRDI QIDQ4304492
Harald Ganzinger, Leo Bachmair
Publication date: 12 September 1994
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/b5a9fe263990670dd0feef306c16001d4993fb92
Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)
Related Items (max. 100)
A first polynomial non-clausal class in many-valued logic ⋮ A strict constrained superposition calculus for graphs ⋮ Unifying splitting ⋮ Equational Theorem Proving for Clauses over Strings ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Towards automated deduction in cP systems ⋮ Superposition for higher-order logic ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ A comprehensive framework for saturation theorem proving ⋮ A comprehensive framework for saturation theorem proving ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ Implementing Superposition in iProver (System Description) ⋮ Make E Smart Again (Short Paper) ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ Beagle – A Hierarchic Superposition Theorem Prover ⋮ On narrowing, refutation proofs and constraints ⋮ Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations ⋮ Automated theorem proving by resolution in non-classical logics ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ The disconnection tableau calculus ⋮ Superposition-based equality handling for analytic tableaux ⋮ Extensional higher-order paramodulation in Leo-III ⋮ On First-Order Model-Based Reasoning ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ Unnamed Item ⋮ An Extension of the Knuth-Bendix Ordering with LPO-Like Properties ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ A rewriting approach to satisfiability procedures. ⋮ Hyperresolution for guarded formulae ⋮ On using ground joinable equations in equational theorem proving ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ Unnamed Item ⋮ Modular proof systems for partial functions with Evans equality ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Ordered tableaux: Extensions and applications ⋮ Deciding expressive description logics in the framework of resolution ⋮ Superposition for Fixed Domains ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Superposition with completely built-in abelian groups ⋮ Congruence Closure with Free Variables ⋮ Redundancy criteria for constrained completion ⋮ SPASS & FLOTTER version 0.42 ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Superposition for Bounded Domains ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Canonical Ground Horn Theories ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ First-Order Resolution Methods for Modal Logics ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Redundancy criteria for constrained completion ⋮ A superposition calculus for abductive reasoning ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Decidability Results for Saturation-Based Model Building ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Predicate Completion for non-Horn Clause Sets ⋮ Fault-Tolerant Aggregate Signatures ⋮ Ordered chaining for total orderings ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ Semantic tableaux with ordering restrictions ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Politeness and combination methods for theories with bridging functions ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Combining induction and saturation-based theorem proving ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Selecting the Selection ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Agent-Based HOL Reasoning ⋮ Equational theorem proving modulo ⋮ Generalized completeness for SOS resolution and its application to a new notion of relevance ⋮ A unifying splitting framework ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Superposition for full higher-order logic ⋮ Neural precedence recommender ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Extending SMT solvers to higher-order logic ⋮ Model completeness, covers and superposition ⋮ Faster, higher, stronger: E 2.3 ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ A term-graph clausal logic: completeness and incompleteness results ★ ⋮ Local simplification ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries ⋮ A Generalisation of the Hyperresolution Principle to First Order Gödel Logic ⋮ Decidability and complexity analysis by basic paramodulation ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Soft typing for ordered resolution ⋮ Unnamed Item ⋮ On the refutational completeness of signed binary resolution and hyperresolution ⋮ Completeness of hyper-resolution via the semantics of disjunctive logic programs ⋮ Hyperresolution for Gödel logic with truth constants
This page was built for publication: Rewrite-based Equational Theorem Proving with Selection and Simplification
