Theorem proving with variable-constrained resolution

DOI10.1016/S0020-0255(72)80012-4zbMath0243.68011MaRDI QIDQ2554609

Yanyan Li

Publication date: 1972

Published in: Information Sciences (Search for Journal in Brave)

Mathematics Subject Classification ID

Related Items

Using rewriting rules for connection graphs to prove theorems, Complexity of resolution proofs and function introduction, On an unsatisfiability-satisfiability prover, What you always wanted to know about rigid E-unification

Cites Work

• Renamable paramodulation for automatic theorem proving with equality
• Finding resolution proofs and using duplicate goals in AND/OR trees
• A Proof Method for Quantification Theory: Its Justification and Realization
• An improved proof procedure1
• Theorem-Proving on the Computer
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• The Concept of Demodulation in Theorem Proving
• Theorem-Proving for Computers: Some Results on Resolution and Renaming
• Mechanical Theorem-Proving by Model Elimination
• Resolution With Merging
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• The Unit Proof and the Input Proof in Theorem Proving
• A Computing Procedure for Quantification Theory
• A Mechanical Proof Procedure and its Realization in an Electronic Computer
• Completeness of Linear Refutation for Theories with Equality
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item