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

DOI10.1016/S0020-0255(71)80013-0zbMATH Open0226.68043MaRDI QIDQ2549243FDOQ2549243

Authors: James R. Slagle, Deena A. Koniver 

Publication date: 1971

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

Mathematics Subject Classification ID

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

Cites Work

• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem-Proving for Computers: Some Results on Resolution and Renaming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Experiments With a Multipurpose, Theorem-Proving Heuristic Program
• Title not available (Why is that?)
• A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
• Experiments in automatic learning for a multipurpose hueristic program
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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)