Paramodulation-based theorem proving
From MaRDI portal
The aim of this chapter is to review the fundamental techniques in paramodulation-based theorem proving and presenting them in a uniform framework. It starts with easier subcases and progressively the different extensions are included. Since the objective is to obtain a concise overview of the current state of the art, some of the historical developments that are not essential for the current results are omitted.NEWLINENEWLINENEWLINEIn the first section, the main concepts are introduced in an informal way, with emphasis on their intuitive background. This is done to facilitate the reading of subsequent sections, where all these notions are formally defined and explained in detail, and some of the main results are proved.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
Recommendations
Cited in
(only showing first 100 items - show all)- Labelled splitting
- A new methodology for developing deduction methods
- Theory decision by decomposition
- Combination of convex theories: modularity, deduction completeness, and explanation
- Practical algorithms for deciding path ordering constraint satisfaction.
- A rewriting approach to satisfiability procedures.
- Stratified resolution
- Superposition with completely built-in abelian groups
- Superposition as a decision procedure for timed automata
- A superposition calculus for abductive reasoning
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Equational theorem proving modulo
- Neural precedence recommender
- Improving ENIGMA-style clause selection while learning from history
- 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
- 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)
- Automated generation of exam sheets for automated deduction
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- AC simplifications and closure redundancies in the superposition calculus
- -paramodulation method for a lattice-valued logic L_nF(X) with equality
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Blocking and other enhancements for bottom-up model generation methods
- Combining induction and saturation-based theorem proving
- Extending SMT solvers to higher-order logic
- Model completeness, covers and superposition
- Induction in saturation-based proof search
- SMELS: satisfiability modulo equality with lazy superposition
- A complete superposition calculus for primal grammars
- Tree automata with equality constraints modulo equational theories
- Resolution with order and selection for hybrid logics
- Decision procedures for extensions of the theory of arrays
- User interaction with the Matita proof assistant
- 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
- Abstract canonical presentations
- Selecting the selection
- Rewrite-based decision procedures
- Rewrite-based satisfiability procedures for recursive data structures
- The power of parameterization in coinductive proof
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- A Lambda-Free Higher-Order Recursive Path Order
- Proof-Relevant Parametricity
- Automated reasoning building blocks
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Quantifier-free equational logic and prime implicate generation
- Multi-completion with termination tools
- Paramodulation with non-monotonic orderings and simplification
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Superposition for Fixed Domains
- Attributed Graph Constraints
- Engineering DPLL(T) + Saturation
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Data structures with arithmetic constraints: A non-disjoint combination
- scientific article; zbMATH DE number 4022665 (Why is no real title available?)
- Superposition Calculus
- Model evolution with equality -- revised and implemented
- On deciding satisfiability by theorem proving with speculative inferences
- scientific article; zbMATH DE number 1538015 (Why is no real title available?)
- scientific article; zbMATH DE number 1765692 (Why is no real title available?)
- 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).
- Implementing Superposition in iProver (System Description)
- Proof normalization for resolution and paramodulation
- Mechanically certifying formula-based Noetherian induction reasoning
- SMT-based verification of data-aware processes: a model-theoretic approach
- Clause set cycles and induction
- Combinable Extensions of Abelian Groups
- Interpolation and Symbol Elimination
- Decidability Results for Saturation-Based Model Building
- System description: SPASS-FD
- Functional logic programming in Maude
- Rewriting interpolants
- A Logic of Graph Constraints
- Automatic decidability and combinability
- Model-theoretic methods in combined constraint satisfiability
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Superposition with lambdas
- A comprehensive framework for saturation theorem proving
- Getting saturated with induction
- Equational Theorem Proving for Clauses over Strings
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- SAT-Based Subsumption Resolution
- Program Synthesis in Saturation
- ALASCA: reasoning in quantified linear arithmetic
- Small term reachability and related problems for terminating term rewriting systems
- Constraint learning for non-confluent proof search
This page was built for publication: Paramodulation-based theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751359)
