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

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, 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

• REDUCE

Cites Work

• 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
• 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