scientific article

Publication date: 27 August 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

equational theories paramodulation-based theorem proving

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (92)

Automated generation of exam sheets for automated deduction ⋮ Vampire with a brain is a good ITP hammer ⋮ Implementing Superposition in iProver (System Description) ⋮ Automated Reasoning Building Blocks ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality ⋮ Multi-completion with termination tools ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ The disconnection tableau calculus ⋮ Superposition-based equality handling for analytic tableaux ⋮ Getting saturated with induction ⋮ Equational Theorem Proving for Clauses over Strings ⋮ Practical algorithms for deciding path ordering constraint satisfaction. ⋮ A rewriting approach to satisfiability procedures. ⋮ Tree automata with equality constraints modulo equational theories ⋮ Stratified resolution ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Resolution with order and selection for hybrid logics ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Model evolution with equality -- revised and implemented ⋮ Superposition as a decision procedure for timed automata ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Superposition for Fixed Domains ⋮ Attributed Graph Constraints ⋮ Connection tableaux with lazy paramodulation ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Engineering DPLL(T) + Saturation ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Superposition with completely built-in abelian groups ⋮ Decision procedures for extensions of the theory of arrays ⋮ User interaction with the Matita proof assistant ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Functional Logic Programming in Maude ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Superposition for Bounded Domains ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ First-Order Resolution Methods for Modal Logics ⋮ Quantifier Elimination and Provers Integration ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ Rewriting Interpolants ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Translation of resolution proofs into short first-order proofs without choice axioms ⋮ Mechanising first-order temporal resolution ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Automatic decidability and combinability ⋮ A superposition calculus for abductive reasoning ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Abstract canonical presentations ⋮ Combinable Extensions of Abelian Groups ⋮ Interpolation and Symbol Elimination ⋮ Decidability Results for Saturation-Based Model Building ⋮ System Description: SPASS-FD ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Satisfiability Procedures for Combination of Theories Sharing Integer Offsets ⋮ A Logic of Graph Constraints ⋮ Superposition with lambdas ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Combining induction and saturation-based theorem proving ⋮ Selecting the Selection ⋮ Equational theorem proving modulo ⋮ Neural precedence recommender ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Extending SMT solvers to higher-order logic ⋮ Model completeness, covers and superposition ⋮ Induction in saturation-based proof search ⋮ Unnamed Item ⋮ Labelled splitting ⋮ A new methodology for developing deduction methods ⋮ Data Structures with Arithmetic Constraints: A Non-disjoint Combination ⋮ Theory decision by decomposition ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Subsumption demodulation in first-order theorem proving ⋮ A comprehensive framework for saturation theorem proving ⋮ Rewrite-Based Decision Procedures ⋮ Rewrite-Based Satisfiability Procedures for Recursive Data Structures ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Semantic relevance ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ SMELS: satisfiability modulo equality with lazy superposition ⋮ A complete superposition calculus for primal grammars

This page was built for publication: