Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
From MaRDI portal
Publication:5507985
DOI10.1145/321296.321302zbMath0135.18401WikidataQ114255236 ScholiaQ114255236MaRDI QIDQ5507985
No author found.
Publication date: 1965
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321296.321302
Related Items
Removing irrelevant information in temporal resolution proofs, MRPPS?An interactive refutation proof procedure system for question-answering, A logical framework for depiction and image interpretation, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), An epistemic model of logic programming, Lightweight relevance filtering for machine-generated resolution problems, A mechanical solution of Schubert's steamroller by many-sorted resolution, Hierarchical deduction, Resolution vs. cutting plane solution of inference problems: Some computational experience, Theorem proving with abstraction, A resolution framework for finitely-valued first-order logics, A semantic backward chaining proof system, A relaxation approach to splitting in an automatic theorem prover, Experimental tests of resolution-based theorem-proving strategies, The kernel strategy and its use for the study of combinatory logic, The resonance strategy, The application of automated reasoning to questions in mathematics and logic, The application of automated reasoning to formal models of combinatorial optimization, A typed resolution principle for deduction with conditional typing theory, Automation for interactive proof: first prototype, Resolution graphs, Finding resolution proofs and using duplicate goals in AND/OR trees, Experiments with a heuristic theorem-proving program for predicate calculus with equality, Linear resolution with selection function, Theorem proving with variable-constrained resolution, Beweisalgorithmen für die Prädikatenlogik, Checking the quality of clinical guidelines using automated reasoning tools, A pragmatic approach to resolution-based theorem proving
