scholarly journals Temporal logic programs with variables

2016 ◽  
Vol 17 (2) ◽  
pp. 226-243 ◽  
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
GILBERTO PÉREZ ◽  
CONCEPCIÓN VIDAL ◽  
MARTÍN DIÉGUEZ
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Logic Program ◽  
Answer Set Programming ◽  
Logic Programs ◽  
First Order ◽  
Linear Time Temporal Logic ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic models we call temporal stable models. Then, we consider a subclass of theories (called splittable temporal logic programs) that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of safe variables that suffices to show the property of domain independence – that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard Answer Set Programming grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

scholarly journals Linear-Time Temporal Answer Set Programming

2021 ◽  
pp. 1-55
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
MARTÍN DIÉGUEZ ◽  
GILBERTO PÉREZ ◽  
TORSTEN SCHAUB ◽  
...  
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Selection Criterion ◽  
Answer Set Programming ◽  
Logic Programs ◽  
Modal Operators ◽  
Linear Time Temporal Logic ◽  
Stable Models ◽  
Answer Set

Abstract In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

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.

scholarly journals Stable models for infinitary formulas with extensional atoms

2016 ◽  
Vol 16 (5-6) ◽  
pp. 771-786
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ
Keyword(s):  
Programming Languages ◽  
Answer Set Programming ◽  
Splitting Theorem ◽  
First Order ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractThe definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions.

scholarly journals Dynamic Linear Time Temporal Logic

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Order Theory ◽  
Simple Extension ◽  
Propositional Dynamic Logic ◽  
First Order ◽  
Time Semantics ◽  
Linear Time Temporal Logic ◽  
Obvious Manner

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.

scholarly journals Knowledge Forgetting in Answer Set Programming

2014 ◽  
Vol 50 ◽  
pp. 31-70 ◽  
Author(s):  
Y. Wang ◽  
Y. Zhang ◽  
Y. Zhou ◽  
M. Zhang
Keyword(s):  
Logic Program ◽  
Answer Set Programming ◽  
Irrelevant Information ◽  
Semantic Knowledge ◽  
Decision Problems ◽  
Stable Model ◽  
Logic Programs ◽  
Knowledge Based ◽  
Substitution Principle ◽  
Answer Set

The ability of discarding or hiding irrelevant information has been recognized as an important feature for knowledge based systems, including answer set programming. The notion of strong equivalence in answer set programming plays an important role for different problems as it gives rise to a substitution principle and amounts to knowledge equivalence of logic programs. In this paper, we uniformly propose a semantic knowledge forgetting, called HT- and FLP-forgetting, for logic programs under stable model and FLP-stable model semantics, respectively. Our proposed knowledge forgetting discards exactly the knowledge of a logic program which is relevant to forgotten variables. Thus it preserves strong equivalence in the sense that strongly equivalent logic programs will remain strongly equivalent after forgetting the same variables. We show that this semantic forgetting result is always expressible; and we prove a representation theorem stating that the HT- and FLP-forgetting can be precisely characterized by Zhang-Zhou's four forgetting postulates under the HT- and FLP-model semantics, respectively. We also reveal underlying connections between the proposed forgetting and the forgetting of propositional logic, and provide complexity results for decision problems in relation to the forgetting. An application of the proposed forgetting is also considered in a conflict solving scenario.

scholarly journals Minish HAT: A Tool for the Minimization of Here-and-There Logic Programs and Theories in Answer Set Programming

Proceedings ◽  
2019 ◽  
Vol 21 (1) ◽  
pp. 22
Author(s):  
Rodrigo Martin ◽  
Pedro Cabalar
Keyword(s):  
Logic Program ◽  
Answer Set Programming ◽  
Boolean Logic ◽  
Minimal Representation ◽  
Logic Programs ◽  
Minimization Methods ◽  
Programming Techniques ◽  
Software Implementations ◽  
Reduced Time ◽  
Answer Set

When it comes to the writing of a new logic program or theory, it is of great importance to obtain a concise and minimal representation, for simplicity and ease of interpretation reasons. There are already a few methods and many tools, such as Karnaugh Maps or the Quine-McCluskey method, as well as their numerous software implementations, that solve this minimization problem in Boolean logic. This is not the case for Here-and-There logic, also called three-valued logic. Even though there are theoretical minimization methods for logic theories and programs, there aren’t any published tools that are able to obtain a minimal equivalent logic program. In this paper we present the first version of a tool called that is able to efficiently obtain minimal and equivalent representations for any logic program in Here-and-There. The described tool uses an hybrid method both leveraging a modified version of the Quine-McCluskey algorithm and Answer Set Programming techniques to minimize fairly complex logic programs in a reduced time.

scholarly journals Optimizing Answer Set Computation via Heuristic-Based Decomposition

2019 ◽  
Vol 19 (04) ◽  
pp. 603-628 ◽  
Author(s):  
FRANCESCO CALIMERI ◽  
SIMONA PERRI ◽  
JESSICA ZANGARI
Keyword(s):  
Logic Programming ◽  
Logic Program ◽  
Answer Set Programming ◽  
Decomposition Techniques ◽  
Logic Programs ◽  
Experimental Activity ◽  
Performance Of Systems ◽  
Answer Sets ◽  
The Impact ◽  
Answer Set

AbstractAnswer Set Programming (ASP) is a purely declarative formalism developed in the field of logic programming and non-monotonic reasoning: computational problems are encoded by logic programs whose answer sets, corresponding to solutions, are computed by an ASP system. Different, semantically equivalent, programs can be defined for the same problem; however, performance of systems evaluating them might significantly vary. We propose an approach for automatically transforming an input logic program into an equivalent one that can be evaluated more efficiently. One can make use of existing tree-decomposition techniques for rewriting selected rules into a set of multiple ones; the idea is to guide and adaptively apply them on the basis of proper new heuristics, to obtain a smart rewriting algorithm to be integrated into an ASP system. The method is rather general: it can be adapted to any system and implement different preference policies. Furthermore, we define a set of new heuristics tailored at optimizing grounding, one of the main phases of the ASP computation; we use them in order to implement the approach into the ASP systemDLV, in particular into its grounding subsystemℐ-DLV, and carry out an extensive experimental activity for assessing the impact of the proposal.

Program completion in the input language of GRINGO

2017 ◽  
Vol 17 (5-6) ◽  
pp. 855-871 ◽  
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ ◽  
DHANANJAY RAJU
Keyword(s):  
Reverse Engineering ◽  
Large Class ◽  
Logic Program ◽  
Answer Set Programming ◽  
Program Completion ◽  
Engineering Process ◽  
Input Language ◽  
Definition Of ◽  
Answer Set

AbstractWe argue that turning a logic program into a set of completed definitions can be sometimes thought of as the “reverse engineering” process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set Programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms with their expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.

scholarly journals Inconsistency Proofs for ASP: The ASP - DRUPE Format

2019 ◽  
Vol 19 (5-6) ◽  
pp. 891-907
Author(s):  
MARIO ALVIANO ◽  
CARMINE DODARO ◽  
JOHANNES K. FICHTE ◽  
MARKUS HECHER ◽  
TOBIAS PHILIPP ◽  
...  
Keyword(s):  
Logic Program ◽  
Answer Set Programming ◽  
Boolean Satisfiability ◽  
Logic Programs ◽  
Disjunctive Logic Programs ◽  
Normal Logic ◽  
Consistency Problem ◽  
Unit Propagation ◽  
Answer Sets ◽  
Answer Set

AbstractAnswer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs.

scholarly journals Relational theories with null values and non-herbrand stable models

2012 ◽  
Vol 12 (4-5) ◽  
pp. 565-582 ◽  
Author(s):  
VLADIMIR LIFSCHITZ ◽  
KARL PICHOTTA ◽  
FANGKAI YANG
Keyword(s):  
Incomplete Information ◽  
Relational Databases ◽  
Logic Program ◽  
Answer Set Programming ◽  
First Order ◽  
Relational Theories ◽  
Null Values ◽  
Closure Assumption ◽  
General Method ◽  
Stable Models

AbstractGeneralized relational theories with null values in the sense of Reiter are first-order theories that provide a semantics for relational databases with incomplete information. In this paper we show that any such theory can be turned into an equivalent logic program, so that models of the theory can be generated using computational methods of answer set programming. As a step towards this goal, we develop a general method for calculating stable models under the domain closure assumption but without the unique name assumption.

Sign in / Sign up

Export Citation Format

Share Document