Non-resolution theorem proving

DOI10.1016/0004-3702(77)90012-1zbMath0358.68131OpenAlexW2023139438MaRDI QIDQ1238434

W. W. Bledsoe

Publication date: 1977

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(77)90012-1

Mathematics Subject Classification ID

Related Items (37)

Conditional term rewriting and first-order theorem proving ⋮ A fully automatic theorem prover with human-style output ⋮ Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures ⋮ History and Prospects for First-Order Automated Deduction ⋮ Consider only general superpositions in completion procedures ⋮ Proofs as Objects ⋮ Hierarchical deduction ⋮ \(M\)-calculus -- a sequent method for automatic theorem proving ⋮ Man-machine theorem proving in graph theory ⋮ Only prime superpositions need be considered in the Knuth-Bendix completion procedure ⋮ Set theory for verification. II: Induction and recursion ⋮ MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics ⋮ Using hints to increase the effectiveness of an automated reasoning program: Case studies ⋮ Unnecessary inferences in associative-commutative completion procedures ⋮ Tautology testing with a generalized matrix reduction method ⋮ Application of the rule of inference in informal mathematical proofs ⋮ A first polynomial non-clausal class in many-valued logic ⋮ Theorem proving with abstraction ⋮ Automated proof of ring commutativity problems by algebraic methods ⋮ A simplified problem reduction format ⋮ An automatic proof of Gödel's incompleteness theorem ⋮ Knowledge-based proof planning ⋮ Banishing Ultrafilters from Our Consciousness ⋮ Specification methods and partial construction of theory by computer ⋮ Analogy in Automated Deduction: A Survey ⋮ Implementation of proof schemes in the method of invariant transformations ⋮ SLIM: An automated reasoner for equivalences, applied to set theory ⋮ An experimental logic based on the fundamental deduction principle ⋮ A pragmatic approach to resolution-based theorem proving ⋮ Human-centered automated proof search ⋮ Partial matching for analogy discovery in proofs and counter-examples ⋮ Building proofs or counterexamples by analogy in a resolution framework ⋮ Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ Refutational theorem proving using term-rewriting systems ⋮ Top-down synthesis of divide-and-conquer algorithms ⋮ Set theory for verification. I: From foundations to functions

Uses Software

• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about programs
• Plane geometry theorem proving using forward chaining
• A relaxation approach to splitting in an automatic theorem prover
• Untersuchungen über das logische Schliessen. I
• The \(Q^*\) algorithm - a search strategy for a deductive question-answering system
• A man-machine theorem-proving system
• The semantics of induction and the possibility of complete systems of inductive inference
• Specialization of the form of deduction in the precicate calculus with equality and function symbols. I
• Splitting and reduction heuristics in automatic theorem proving
• A paradigm for reasoning by analogy
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• Computer proofs of limit theorems
• Breadth-first search: some surprising results
• Experiment with an automatic theorem-prover having partial ordering inference rules
• An improved proof procedure1
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Semantically Guided Deductive System for Automatic Theorem Proving
• Semantic Resolution for Horn Sets
• A Human Oriented Logic for Automatic Theorem-Proving
• Proving Theorems about LISP Functions
• A New Class of Automated Theorem-Proving Algorithms
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Semi-Automated Mathematics
• Notes on central groupoids
• Applications of symbol manipulation in theoretical physics
• Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets

This page was built for publication: Non-resolution theorem proving