Theorem proving with variable-constrained resolution

DOI10.1016/S0020-0255(72)80012-4MaRDI QIDQ2554609zbMATH OpenFDO

Authors Yanyan Li

Publication date 1972

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0020-0255(72)80012-4

Mathematics Subject Classification ID

Cites work

• A Computing Procedure for Quantification Theory
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A Machine-Oriented Logic Based on the Resolution Principle
• A Mechanical Proof Procedure and its Realization in an Electronic Computer
• A Proof Method for Quantification Theory: Its Justification and Realization
• An improved proof procedure1
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Completeness of Linear Refutation for Theories with Equality
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Finding resolution proofs and using duplicate goals in AND/OR trees
• scientific article; zbMATH DE number 3212023 (Why is no real title available?)
• scientific article; zbMATH DE number 3219316 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3310921 (Why is no real title available?)
• scientific article; zbMATH DE number 3313862 (Why is no real title available?)
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3346109 (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 3407195 (Why is no real title available?)
• Mechanical Theorem-Proving by Model Elimination
• Renamable paramodulation for automatic theorem proving with equality
• Resolution With Merging
• The Concept of Demodulation in Theorem Proving
• The Unit Proof and the Input Proof in Theorem Proving
• Theorem-Proving for Computers: Some Results on Resolution and Renaming
• Theorem-Proving on the Computer

Cited in

(4)

• 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

This page was built for publication: Theorem proving with variable-constrained resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2554609)