“Dynamic” inferencing with generalized resolution
References
Index Terms
- “Dynamic” inferencing with generalized resolution
Recommendations
Monodic temporal resolution
Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a ...
I-terms in ordered resolution and superposition calculi: retrieving lost completeness
AISC'10/MKM'10/Calculemus'10: Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematicsOrdered resolution and superposition are the state-of-the-art proof procedures used in saturation-based theorem proving, for non equational and equational clause sets respectively. In this paper, we present extensions of these calculi that permit one to ...
Extensional Higher-Order Paramodulation in Leo-III
AbstractLeo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Reviews
Victor W. Marek
Some well-known techniques in automated theorem proving for propositional logic are reviewed. The authors compare Robinson's resolution method with Smullyan's semantic tableau method, Hao Wang's Gentzen-style technique, Murray's nonclausal resolution, and Hilbert's method. The authors notice that resolution and tableaux possess dual techniques. They discuss these as well. Unfortunately, the authors completely avoid the complexity issues associated with these methods. This is a major omission, because of the central place of provability (and its dual, satisfiability) in the complexity theory. The paper reads well, but does not go beyond an exercise in automated theorem proving.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Check for updates
Author Tags
Qualifiers
- Article
Conference
Acceptance Rates
Upcoming Conference
- Sponsor:
- sigapp
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 239Total Downloads
- Downloads (Last 12 months)38
- Downloads (Last 6 weeks)8
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in