The Unit Proof and the Input Proof in Theorem Proving
From MaRDI portal
Cited in
(15)- On solving the equality problem in theories defined by Horn clauses
- Complexity and related enhancements for automated theorem-proving programs
- Problem representations and formal properties of heuristic search
- Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
- Experiments with a heuristic theorem-proving program for predicate calculus with equality
- Theorem proving with variable-constrained resolution
- A note on linear resolution strategies in consequence-finding
- Breadth-first search: some surprising results
- Achieving consistency with cutting planes
- MRPPS?An interactive refutation proof procedure system for question-answering
- Representations of the language recognition problem for a theorem prover
- Exploiting parallelism: highly competitive semantic tree theorem prover
- DRAT and propagation redundancy proofs without new variables
- On generalized Horn formulas and k-resolution
- Unit refutability of Horn constraint systems -- certification and parallel complexity
This page was built for publication: The Unit Proof and the Input Proof in Theorem Proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5613968)
