scientific article; zbMATH DE number 3219316
From MaRDI portal
Publication:5507984
Cited in
(20)- A superposition oriented theorem prover
- A resolution framework for finitely-valued first-order logics
- Experimental tests of resolution-based theorem-proving strategies
- Analytic resolution in theorem proving
- On resolution with short clauses
- The Q^* algorithm - a search strategy for a deductive question-answering system
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Resolution graphs
- Finding resolution proofs and using duplicate goals in AND/OR trees
- Theorem proving with variable-constrained resolution
- Beweisalgorithmen für die Prädikatenlogik
- History and prospects for first-order automated deduction
- Removing irrelevant information in temporal resolution proofs
- MRPPS?An interactive refutation proof procedure system for question-answering
- The strategy challenge in SMT solving
- Automatic theorem proving in paraconsistent logics: Theory and implementation
- A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
- Filter-based resolution principle for lattice-valued propositional logic LP(X)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5507984)
