Paramodulation-based theorem proving
From MaRDI portal
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?)
- 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
- Finding connections via satisfiability solving
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)
