Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

1965/10/01 by Lawrence Wos, L. Wos, George A. Robinson +2 · 9 citations
Computer Science · #Logic, programming, and type systems #Quantum Computing Algorithms and Architecture #semigroups and automata theory

paper · pdf · doi:10.1145/321296.321302

Abstract

One of the major problems in mechanical theorem proving is the generation of a plethora of redundant and irrelevant information. To use computers effectively for obtaining proofs, it is necessary to find strategies which will materially impede the generation of irrelevant inferences. One strategy wilich achieves this end is the set of support strategy. With any such strategy two questions of primary interest are that of its efficiency and that of its logical completeness. Evidence of the efficiency of this strategy is presented, and a theorem giving sufficient conditions for its logical completeness is proved.

Cited by

• Properties and Extensions of Alternating Path Relevance - I
• A new perspective of paramodulation complexity by solving massive 8 puzzles
• Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
• Checking the Quality of Clinical Guidelines using Automated Reasoning Tools
• Inconsistency Robustness in Logic Programs
• Dynamic Automated Deduction by Contradiction Separation: The Standard Extension Algorithm
• Some Experiments with Twee-Style Goal-Directedness
• Contradictions
• Layered Clause Selection for Theory Reasoning : (Short Paper) [europepmc]

Related

• Rare Speed-up in Automatic Theorem Proving Reveals Tradeoff Between Computational Time and Information Value
• A Survey on Theorem Provers in Formal Methods
• Automatic Proof Checking and Proof Construction by Tactics
• Top-down Automated Theorem Proving (Notes for Sir Timothy)
• On the Computational Properties of Obviously Strategy-Proof Mechanisms