Theorem-proving with resolution and superposition
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 3924139 (Why is no real title available?)
- scientific article; zbMATH DE number 3928346 (Why is no real title available?)
- scientific article; zbMATH DE number 4049135 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A superposition oriented theorem prover
- On word problems in Horn theories
- Orderings for term-rewriting systems
- Problem corner: Reasoning about equality
- Proving refutational completeness of theorem-proving strategies
- Termination of rewriting
- The Concept of Demodulation in Theorem Proving
- Unit Refutations and Horn Sets
Cited in
(38)- Associative-commutative deduction with constraints
- Using forcing to prove completeness of resolution and paramodulation
- Theorem proving with ordering and equality constrained clauses
- Regular Derivations in Basic Superposition-Based Calculi
- Rewrite method for theorem proving in first order theory with equality
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A superposition oriented theorem prover
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Positive deduction modulo regular theories
- Proving refutational completeness of theorem-proving strategies
- scientific article; zbMATH DE number 4041864 (Why is no real title available?)
- scientific article; zbMATH DE number 4049137 (Why is no real title available?)
- scientific article; zbMATH DE number 1696762 (Why is no real title available?)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Resolution-Like Theorem Proving for High-Level Conditions
- On deciding satisfiability by theorem proving with speculative inferences
- Towards a foundation of completion procedures as semidecision procedures
- scientific article; zbMATH DE number 4089522 (Why is no real title available?)
- On word problems in Horn theories
- scientific article; zbMATH DE number 4022667 (Why is no real title available?)
- scientific article; zbMATH DE number 4049134 (Why is no real title available?)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- A rewriting approach to satisfiability procedures.
- On Arbitrary Selection Strategies for Basic Superposition
- On First-Order Model-Based Reasoning
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- Reasoning with conditional axioms
- Resolution theorem proving
- Observational proofs by rewriting.
- On subsumption in distributed derivations
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- From search to computation: redundancy criteria and simplification at work
- Abstract canonical presentations
- On Theorem Proving in Annotated Logics
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
- On first-order theorem proving using generalized odd-superpositions II
This page was built for publication: Theorem-proving with resolution and superposition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q757094)
