Resolution theorem proving
From MaRDI portal
The paper gives an extensive overview on resolution-based theorem proving. It discusses various resolution refinements and resolution strategies (by introducing orderings) for improving efficiency, and for dealing with special classes of clauses. First-order resolution methods can then be derived from ground resolution and the technique of ``lifting.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
Recommendations
Cited in
(only showing first 100 items - show all)- Lightweight relevance filtering for machine-generated resolution problems
- Labelled splitting
- A new methodology for developing deduction methods
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Deciding H₁ by resolution
- Application of the strategy of ordering disjunctives for a modification of the method of resolutions
- A resolution framework for finitely-valued first-order logics
- \(T\)-resolution: Refinements and model elimination
- Elimination of self-resolving clauses
- Stratified resolution
- Limited resource strategy in resolution theorem proving
- Hyperresolution for guarded formulae
- Limits of theory sequences over algebraically closed fields and applications.
- Theorem proving based on the extension rule
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Automated deduction by theory resolution
- T-theorem proving. I
- Superposition as a decision procedure for timed automata
- A unifying splitting framework
- Superposition with first-class booleans and inprocessing clausification
- Confidences for commonsense reasoning
- Neural precedence recommender
- Improving ENIGMA-style clause selection while learning from history
- Subsumption demodulation in first-order theorem proving
- Layered clause selection for theory reasoning (short paper)
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
- Semantic relevance
- GK: implementing full first order default logic for commonsense reasoning (system description)
- The possibilistic Horn non-clausal knowledge bases
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- 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
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- GKC: a reasoning system for large knowledge bases
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Resolution in solving graph problems
- SMELS: satisfiability modulo equality with lazy superposition
- The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies
- Alternating two-way AC-tree automata
- The model evolution calculus as a first-order DPLL method
- Scavenger 0.1: a theorem prover based on conflict resolution
- Resolution with order and selection for hybrid logics
- ABox abduction in the description logic \(\mathcal{ALC}\)
- Reasoning on UML class diagrams
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Mechanising first-order temporal resolution
- Abstract canonical presentations
- Extracting unsatisfiable cores for LTL via temporal resolution
- Reliability of mathematical inference
- Theorem proving using clausal resolution: from past to present
- Paramodulation-based theorem proving
- Selecting the selection
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Lifting QBF resolution calculi to DQBF
- Understanding Resolution Proofs through Herbrand’s Theorem
- Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies
- Semi-intelligible Isar proofs from machine-generated proofs
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- First-order logic theorem proving and model building via approximation and instantiation
- On the computational complexity of read once resolution decidability in 2CNF formulas
- scientific article; zbMATH DE number 2084332 (Why is no real title available?)
- Decision Procedures for Automating Termination Proofs
- scientific article; zbMATH DE number 3876643 (Why is no real title available?)
- Automated reasoning building blocks
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- History and prospects for first-order automated deduction
- Cooperating proof attempts
- Towards the compression of first-order resolution proofs by lowering unit clauses
- Disproving using the inverse method by iterative refinement of finite approximations
- Ordered resolution for coalition logic
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Case splitting in an automatic theorem prover for real-valued special functions
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Resolution-Like Theorem Proving for High-Level Conditions
- Engineering DPLL(T) + Saturation
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Boundary Points and Resolution
- Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations
- Combining instance generation and resolution
- scientific article; zbMATH DE number 3940761 (Why is no real title available?)
- scientific article; zbMATH DE number 4022664 (Why is no real title available?)
- scientific article; zbMATH DE number 4022667 (Why is no real title available?)
- On Different Concepts of Resolution
- scientific article; zbMATH DE number 4089522 (Why is no real title available?)
- scientific article; zbMATH DE number 4108722 (Why is no real title available?)
- scientific article; zbMATH DE number 8781 (Why is no real title available?)
- scientific article; zbMATH DE number 4128784 (Why is no real title available?)
- The Ackermann approach for modal logic, correspondence theory and second-order reduction
- scientific article; zbMATH DE number 976360 (Why is no real title available?)
- scientific article; zbMATH DE number 1948188 (Why is no real title available?)
- scientific article; zbMATH DE number 2079834 (Why is no real title available?)
- scientific article; zbMATH DE number 1507183 (Why is no real title available?)
- scientific article; zbMATH DE number 1765659 (Why is no real title available?)
- scientific article; zbMATH DE number 2169302 (Why is no real title available?)
- scientific article; zbMATH DE number 910745 (Why is no real title available?)
This page was built for publication: Resolution theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751353)
