Non-resolution theorem proving
From MaRDI portal
Cites work
- A Human Oriented Logic for Automatic Theorem-Proving
- A man-machine theorem-proving system
- A New Class of Automated Theorem-Proving Algorithms
- A paradigm for reasoning by analogy
- A relaxation approach to splitting in an automatic theorem prover
- A Semantically Guided Deductive System for Automatic Theorem Proving
- An improved proof procedure1
- Applications of symbol manipulation in theoretical physics
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Breadth-first search: some surprising results
- Computer proofs of limit theorems
- Experiment with an automatic theorem-prover having partial ordering inference rules
- Experiments with a heuristic theorem-proving program for predicate calculus with equality
- scientific article; zbMATH DE number 3821125 (Why is no real title available?)
- scientific article; zbMATH DE number 3507979 (Why is no real title available?)
- scientific article; zbMATH DE number 3441640 (Why is no real title available?)
- scientific article; zbMATH DE number 3231608 (Why is no real title available?)
- scientific article; zbMATH DE number 3241715 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3301426 (Why is no real title available?)
- scientific article; zbMATH DE number 3309508 (Why is no real title available?)
- scientific article; zbMATH DE number 3339447 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- scientific article; zbMATH DE number 3349334 (Why is no real title available?)
- scientific article; zbMATH DE number 3403724 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- scientific article; zbMATH DE number 3418636 (Why is no real title available?)
- scientific article; zbMATH DE number 3185223 (Why is no real title available?)
- Notes on central groupoids
- Plane geometry theorem proving using forward chaining
- Proving Theorems about LISP Functions
- Reasoning about programs
- Semantic Resolution for Horn Sets
- Semi-Automated Mathematics
- Specialization of the form of deduction in the precicate calculus with equality and function symbols. I
- Splitting and reduction heuristics in automatic theorem proving
- The Q^* algorithm - a search strategy for a deductive question-answering system
- The semantics of induction and the possibility of complete systems of inductive inference
- Untersuchungen über das logische Schliessen. I
Cited in
(37)- Top-down synthesis of divide-and-conquer algorithms
- Hierarchical deduction
- Man-machine theorem proving in graph theory
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
- Tautology testing with a generalized matrix reduction method
- Theorem proving with abstraction
- A simplified problem reduction format
- Set theory for verification. I: From foundations to functions
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- 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
- M-calculus -- a sequent method for automatic theorem proving
- Set theory for verification. II: Induction and recursion
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Knowledge-based proof planning
- Human-centered automated proof search
- A fully automatic theorem prover with human-style output
- Implementation of proof schemes in the method of invariant transformations
- Banishing ultrafilters from our consciousness
- Specification methods and partial construction of theory by computer
- History and prospects for first-order automated deduction
- Unnecessary inferences in associative-commutative completion procedures
- Application of the rule of inference in informal mathematical proofs
- A pragmatic approach to resolution-based theorem proving
- Consider only general superpositions in completion procedures
- Proofs as Objects
- Partial matching for analogy discovery in proofs and counter-examples
- Building proofs or counterexamples by analogy in a resolution framework
- Analogy in automated deduction: a survey
- An experimental logic based on the fundamental deduction principle
- Conditional term rewriting and first-order theorem proving
- An automatic proof of Gödel's incompleteness theorem
- A first polynomial non-clausal class in many-valued logic
- SLIM: An automated reasoner for equivalences, applied to set theory
- Refutational theorem proving using term-rewriting systems
- Automated proof of ring commutativity problems by algebraic methods
This page was built for publication: Non-resolution theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1238434)
