Resolution theorem proving
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Confidences for commonsense reasoning
- Neural precedence recommender
- Superposition with first-class booleans and inprocessing clausification
- MetiTarski: An Automatic Prover for the Elementary Functions
- Limited resource strategy in resolution theorem proving
- scientific article; zbMATH DE number 2169302 (Why is no real title available?)
- Partial redundancy in saturation
- Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
- scientific article; zbMATH DE number 1765659 (Why is no real title available?)
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- A resolution framework for finitely-valued first-order logics
- Case splitting in an automatic theorem prover for real-valued special functions
- From search to computation: redundancy criteria and simplification at work
- A comprehensive framework for saturation theorem proving
- Decidability Results for Saturation-Based Model Building
- SAT-Based Subsumption Resolution
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- Verified Given Clause Procedures
- First order Büchi automata and their application to verification of LTL specifications
- Consequence-based and fixed-parameter tractable reasoning in description logics
- Superposition as a decision procedure for timed automata
- Cooperating proof attempts
- scientific article; zbMATH DE number 2084332 (Why is no real title available?)
- The model evolution calculus as a first-order DPLL method
- Superposition with equivalence reasoning and delayed clause normal form transformation
- On the computational complexity of read once resolution decidability in 2CNF formulas
- Abstract canonical presentations
- scientific article; zbMATH DE number 3940761 (Why is no real title available?)
- scientific article; zbMATH DE number 4022664 (Why is no real title available?)
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- scientific article; zbMATH DE number 2222011 (Why is no real title available?)
- First-order resolution methods for modal logics
- Disproving using the inverse method by iterative refinement of finite approximations
- Ordered resolution for coalition logic
- History and prospects for first-order automated deduction
- Towards the compression of first-order resolution proofs by lowering unit clauses
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
- scientific article; zbMATH DE number 3876643 (Why is no real title available?)
- A first polynomial non-clausal class in many-valued logic
- Linking focusing and resolution with selection
- On Different Concepts of Resolution
- Labelled splitting
- Reliability of mathematical inference
- Theorem proving using clausal resolution: from past to present
- Mechanically certifying formula-based Noetherian induction reasoning
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Recognizing textual entailment by theorem proving approach
- SAT-Inspired Eliminations for Superposition
- A unifying splitting framework
- A resolution calculus for the branching-time temporal logic CTL
- Planning with effectively propositional logic
- ALASCA: reasoning in quantified linear arithmetic
- Lemmas: generation, selection, application
- scientific article; zbMATH DE number 4108722 (Why is no real title available?)
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies
- Engineering DPLL(T) + Saturation
- Combining induction and saturation-based theorem proving
- scientific article; zbMATH DE number 1948188 (Why is no real title available?)
- Semantic relevance
- Constructing Bachmair-Ganzinger models
- Resolution in solving graph problems
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Blocking and other enhancements for bottom-up model generation methods
- Fair Derivations in Monodic Temporal Reasoning
- Extracting unsatisfiable cores for LTL via temporal resolution
- 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
- GK: implementing full first order default logic for commonsense reasoning (system description)
- The possibilistic Horn non-clausal knowledge bases
- Optimized query rewriting for OWL 2 QL
- Theorem proving based on the extension rule
- Vampire with a brain is a good ITP hammer
- GKC: a reasoning system for large knowledge bases
- Understanding Resolution Proofs through Herbrand’s Theorem
- Rewriting Conjunctive Queries over Description Logic Knowledge Bases
- Scavenger 0.1: a theorem prover based on conflict resolution
- A new methodology for developing deduction methods
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Deciding expressive description logics in the framework of resolution
- Mechanising first-order temporal resolution
- Stratified resolution
- The Ackermann approach for modal logic, correspondence theory and second-order reduction
- The blossom of finite semantic trees
- Decision Procedures for Automating Termination Proofs
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Linearity and regularity with negation normal form
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies
- Binary resolution over Boolean lattices
- scientific article; zbMATH DE number 4128784 (Why is no real title available?)
- Application of the strategy of ordering disjunctives for a modification of the method of resolutions
- Alternating two-way AC-tree automata
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Harald Ganzinger's legacy: contributions to logics and programming
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- ABox abduction in the description logic \(\mathcal{ALC}\)
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)
