A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING

2004 ◽  
Vol 15 (02) ◽  
pp. 417-443 ◽  
Author(s):  
MANOLIS GERGATSOULIS ◽  
CHRISTOS NOMIKOS
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Temporal Logic ◽  
Programming Language ◽  
Branching Time ◽  
Logic Programs ◽  
Temporal Logic Programming ◽  
Time Logic ◽  
Proof Procedure ◽  
Resolution Proof

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.

RECOGNIZING NON-FLOUNDERING LOGIC PROGRAMS AND GOALS

1990 ◽  
Vol 01 (02) ◽  
pp. 151-163 ◽  
Author(s):  
ROBERTO BARBUTI ◽  
MAURIZIO MARTELLI
Keyword(s):  
Logic Programming ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Negation As Failure ◽  
Proof Procedure ◽  
Resolution Proof

The introduction of negation in Logic Programming using the Negation as Failure Rule causes some problems regarding the completeness of the SLDNF-Resolution proof procedure. One of the causes of incompleteness arises when evaluating a non-ground negative literal. This is solved by forbidding these evaluations. Obviously, there is the possibility of having only non-ground negative literals in the goal (the floundering of the goal). There is a class of programs and goals (allowed) that has been proved to have the non-floundering property. In this paper an algorithm is proposed which recognizes a wider class of programs with this property and which is based on abstract interpretation techniques.

The relation between logic programming and logic specification

1984 ◽  
Vol 312 (1522) ◽  
pp. 345-361 ◽  
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Specification Language ◽  
Formal Logic ◽  
Automated Deduction ◽  
Logic Programs ◽  
Computing Science ◽  
Complete Specification ◽  
Representation Of Knowledge

Formal logic is widely accepted as a program specification language in computing science. It is ideally suited to the representation of knowledge and the description of problems without regard to the choice of programming language. Its use as a specification language is compatible not only with conventional programming languages but also with programming languages based entirely on logic itself. In this paper I shall investigate the relation that holds when both programs and program specifications are expressed in formal logic. In many cases, when a specification completely defines the relations to be computed, there is no syntactic distinction between specification and program. Moreover the same mechanism that is used to execute logic programs, namely automated deduction, can also be used to execute logic specifications. Thus all relations defined by complete specifications are executable. The only difference between a complete specification and a program is one of efficiency. A program is more efficient than a specification.

Sign in / Sign up

Export Citation Format

Share Document