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