The following pages link to Resolution theorem proving (Q2751353):
Displaying 50 items.
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) (Q2238693) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
- GKC: a reasoning system for large knowledge bases (Q2305438) (← links)
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF (Q2323446) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies (Q2352492) (← links)
- Alternating two-way AC-tree automata (Q2373699) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Resolution with order and selection for hybrid logics (Q2429982) (← links)
- ABox abduction in the description logic \(\mathcal{ALC}\) (Q2429984) (← links)
- Reasoning on UML class diagrams (Q2457652) (← links)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically (Q2484410) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Mechanising first-order temporal resolution (Q2486579) (← links)
- Abstract canonical presentations (Q2500482) (← links)
- Reliability of mathematical inference (Q2695405) (← links)
- Theorem proving using clausal resolution: from past to present (Q2695485) (← links)
- Paramodulation-based theorem proving (Q2751359) (← links)
- Selecting the Selection (Q2817931) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Lifting QBF Resolution Calculi to DQBF (Q2818035) (← links)
- Understanding Resolution Proofs through Herbrand’s Theorem (Q2851942) (← links)
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Q2964454) (← links)
- On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas (Q2988835) (← links)
- Decision Procedures for Automating Termination Proofs (Q3075496) (← links)
- Automated Reasoning Building Blocks (Q3449631) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations (Q3455767) (← links)
- Ordered Resolution for Coalition Logic (Q3455769) (← links)
- Extending a Resolution Prover for Inequalities on Elementary Functions (Q3498456) (← links)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
- Resolution-Like Theorem Proving for High-Level Conditions (Q3540406) (← links)
- Engineering DPLL(T) + Saturation (Q3541724) (← links)
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables (Q3631368) (← links)
- Boundary Points and Resolution (Q3637164) (← links)
- Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations (Q3637268) (← links)
- Combining Instance Generation and Resolution (Q3655208) (← links)
- (Q3711782) (← links)
- On Different Concepts of Resolution (Q3789526) (← links)
- Another technique for proving completeness of ground resolution (Q3971269) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- The Blossom of Finite Semantic Trees (Q4916075) (← links)
- From Search to Computation: Redundancy Criteria and Simplification at Work (Q4916077) (← links)
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) (← links)
- Constructing Bachmair-Ganzinger Models (Q4916082) (← links)
- Planning with Effectively Propositional Logic (Q4916083) (← links)
