scientific article; zbMATH DE number 3219316
From MaRDI portal
Publication:5507984
zbMath0135.18306MaRDI QIDQ5507984
No author found.
Publication date: 1964
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (19)
History and Prospects for First-Order Automated Deduction ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ On resolution with short clauses ⋮ A resolution framework for finitely-valued first-order logics ⋮ The Strategy Challenge in SMT Solving ⋮ Experimental tests of resolution-based theorem-proving strategies ⋮ Analytic resolution in theorem proving ⋮ Removing irrelevant information in temporal resolution proofs ⋮ Resolution graphs ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ Finding resolution proofs and using duplicate goals in AND/OR trees ⋮ Theorem proving with variable-constrained resolution ⋮ Beweisalgorithmen für die Prädikatenlogik ⋮ The \(Q^*\) algorithm - a search strategy for a deductive question-answering system ⋮ A superposition oriented theorem prover ⋮ 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 ⋮ MRPPS?An interactive refutation proof procedure system for question-answering
This page was built for publication: