scholarly journals Temporal logic programming

1989 ◽  
Vol 8 (3) ◽  
pp. 277-295 ◽  
Author(s):  
Martín Abadi ◽  
Zohar Manna
Keyword(s):  
Logic Programming ◽  
Temporal Logic ◽  
Temporal Logic Programming

scholarly journals Framed temporal logic programming

2008 ◽  
Vol 70 (1) ◽  
pp. 31-61 ◽  
Author(s):  
Zhenhua Duan ◽  
Xiaoxiao Yang ◽  
Maciej Koutny
Keyword(s):  
Logic Programming ◽  
Temporal Logic ◽  
Temporal Logic Programming

An infinitary encoding of temporal equilibrium logic

2015 ◽  
Vol 15 (4-5) ◽  
pp. 666-680 ◽  
Author(s):  
PEDRO CABALAR ◽  
MARTÍN DIÉGUEZ ◽  
CONCEPCIÓN VIDAL
Keyword(s):  
Logic Programming ◽  
Temporal Logic ◽  
Linear Time ◽  
Answer Set Programming ◽  
Modal Operators ◽  
Temporal Logic Programming ◽  
Linear Time Temporal Logic ◽  
Answer Set

AbstractThis paper studies the relation between two recent extensions of propositional Equilibrium Logic, a well-known logical characterisation of Answer Set Programming. In particular, we show how Temporal Equilibrium Logic, which introduces modal operators as those typically handled in Linear-Time Temporal Logic (LTL), can be encoded into Infinitary Equilibrium Logic, a recent formalisation that allows the use of infinite conjunctions and disjunctions. We prove the correctness of this encoding and, as an application, we further use it to show that the semantics of the temporal logic programming formalism called TEMPLOG is subsumed by Temporal Equilibrium Logic.

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.

Sign in / Sign up

Export Citation Format

Share Document