Bibliographic Details
| Title: |
A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING. |
| Authors: |
Gergatsoulis, Manolis1 manolis@ionio.gr, Nomikos, Christos2 cnomikos@cs.uoi.gr |
| Source: |
International Journal of Foundations of Computer Science. Apr2004, Vol. 15 Issue 2, p417-443. 27p. |
| Subjects: |
Logic programming, Programming languages, Electronic data processing, Proof theory, Mathematical logic, Automatic theorem proving |
| Abstract: |
In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs. [ABSTRACT FROM AUTHOR] |
|
Copyright of International Journal of Foundations of Computer Science is the property of World Scientific Publishing Company and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
