Finding resolution proofs and using duplicate goals in AND/OR trees

DOI10.1016/S0020-0255(71)80013-0MaRDI QIDQ2549243zbMATH OpenFDO

Authors James R. Slagle, Deena A. Koniver

Publication date 1971

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0020-0255(71)80013-0

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to computer science (68-04)

Cites work

• A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Experiments in automatic learning for a multipurpose hueristic program
• Experiments With a Multipurpose, Theorem-Proving Heuristic Program
• scientific article; zbMATH DE number 3219315 (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 3275610 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3298341 (Why is no real title available?)
• scientific article; zbMATH DE number 3310099 (Why is no real title available?)
• scientific article; zbMATH DE number 3332896 (Why is no real title available?)
• scientific article; zbMATH DE number 3331276 (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 3185223 (Why is no real title available?)
• Theorem-Proving for Computers: Some Results on Resolution and Renaming

Cited in

(3)

• An admissible and optimal algorithm for searching AND/OR graphs
• Theorem proving with variable-constrained resolution
• Representations of the language recognition problem for a theorem prover

This page was built for publication: Finding resolution proofs and using duplicate goals in AND/OR trees

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