Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
From MaRDI portal
Publication:5507985
DOI10.1145/321296.321302zbMath0135.18401OpenAlexW1972956465WikidataQ114255236 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
Semantically-guided goal-sensitive reasoning: model representation, The resonance strategy, Goal directed strategies for paramodulation, Hierarchical deduction, The application of automated reasoning to questions in mathematics and logic, Resolution vs. cutting plane solution of inference problems: Some computational experience, Case splitting in an automatic theorem prover for real-valued special functions, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), On First-Order Model-Based Reasoning, On structures of regular standard contradictions in propositional logic, Contradiction separation based dynamic multi-clause synergized automated deduction, Theorem proving with abstraction, Unnamed Item, Automation for interactive proof: first prototype, Semantically-guided goal-sensitive reasoning: inference system and completeness, First-order automated reasoning with theories: when deduction modulo theory meets practice, An epistemic model of logic programming, Checking the quality of clinical guidelines using automated reasoning tools, A resolution framework for finitely-valued first-order logics, A semantic backward chaining proof system, The Strategy Challenge in SMT Solving, Canonical Ground Horn Theories, A relaxation approach to splitting in an automatic theorem prover, Sledgehammer: Judgement Day, Experimental tests of resolution-based theorem-proving strategies, A logical framework for depiction and image interpretation, Removing irrelevant information in temporal resolution proofs, A pragmatic approach to resolution-based theorem proving, Lightweight relevance filtering for machine-generated resolution problems, The search efficiency of theorem proving strategies, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, : A Resolution-Based Prover for Multimodal K, Generalized completeness for SOS resolution and its application to a new notion of relevance, 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, Layered clause selection for theory reasoning (short paper), The application of automated reasoning to formal models of combinatorial optimization, A typed resolution principle for deduction with conditional typing theory, A mechanical solution of Schubert's steamroller by many-sorted resolution, 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, The kernel strategy and its use for the study of combinatory logic, Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL, Semantic relevance, MRPPS?An interactive refutation proof procedure system for question-answering
