Knowledge Forgetting in Answer Set Programming

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.

Download Full-text

Query Answering with Guarded Existential Rules under Stable Model Semantics

Proceedings of the AAAI Conference on Artificial Intelligence ◽

10.1609/aaai.v34i03.5695 ◽

2020 ◽

Vol 34 (03) ◽

pp. 3017-3024

Author(s):

Hai Wan ◽

Guohui Xiao ◽

Chenglin Wang ◽

Xianqiao Liu ◽

Junhong Chen ◽

...

Keyword(s):

Answer Set Programming ◽

Query Answering ◽

Prototype System ◽

Stable Model ◽

Logic Programs ◽

Termination Problem ◽

Answer Set

In this paper, we study the problem of query answering with guarded existential rules (also called GNTGDs) under stable model semantics. Our goal is to use existing answer set programming (ASP) solvers. However, ASP solvers handle only finitely-ground logic programs while the program translated from GNTGDs by Skolemization is not in general. To address this challenge, we introduce two novel notions of (1) guarded instantiation forest to describe the instantiation of GNTGDs and (2) prime block to characterize the repeated infinitely-ground program translated from GNTGDs. Using these notions, we prove that the ground termination problem for GNTGDs is decidable. We also devise an algorithm for query answering with GNTGDs using ASP solvers. We have implemented our approach in a prototype system. The evaluation over a set of benchmarks shows encouraging results.

Download Full-text

A decidable subclass of finitary programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068410000232 ◽

2010 ◽

Vol 10 (4-6) ◽

pp. 481-496 ◽

Cited By ~ 8

Author(s):

SABRINA BASELICE ◽

PIERO A. BONATTI

Keyword(s):

Problem Solving ◽

Answer Set Programming ◽

Stable Model ◽

Unique Combination ◽

Logic Programs ◽

Trade Off ◽

Full Support ◽

Odd Cycles ◽

Answer Set

AbstractAnswer set programming—the most popular problem solving paradigm based on logic programs—has been recently extended to support uninterpreted function symbols (Syrjänen 2001, Bonatti 2004; Simkus and Eiter 2007; Gebseret al. 2007; Baseliceet al. 2009; Calimeriet al. 2008). All of these approaches have some limitation. In this paper we propose a class of programs called FP2 that enjoys a different trade-off between expressiveness and complexity. FP2 is inspired by the extension of finitary normal programs with local variables introduced in (Bonatti 2004, Section 5). FP2 programs enjoy the following unique combination of properties: (i) the ability of expressing predicates with infinite extensions; (ii) full support for predicates with arbitrary arity; (iii) decidability of FP2 membership checking; (iv) decidability of skeptical and credulous stable model reasoning for call-safe queries. Odd cycles are supported by composing FP2 programs with argument restricted programs.

Download Full-text

A Case for Query-driven Predicate Answer Set Programming

10.29007/ngm2 ◽

2018 ◽

Author(s):

Gopal Gupta ◽

Elmer Salazar ◽

Kyle Marple ◽

Zhuo Chen ◽

Farhad Shakerin

Keyword(s):

Logic Programming ◽

Common Sense ◽

Automated Reasoning ◽

Answer Set Programming ◽

Stable Model ◽

Common Sense Reasoning ◽

Knowledge Based ◽

Full Power ◽

Programming Systems ◽

Answer Set

Answer Set Programming (ASP) has emerged as a successful paradigm for developing intelligent applications. ASP is based on adding negation as failure to logic programming under the stable model semantics regime. ASP allows for sophisticated reasoning mechanisms that are employed by humans to be modeled elegantly. We argue that being able to model common sense reasoning as used by humans is critical for success of automated reasoning. We also argue that extending answer programming systems to general predicates is critical to realizing the full power of ASP. Goal-directed predicate ASP systems are needed to make the ASP technology practical for building large, scalable knowledge-based applications.

Download Full-text

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

Proceedings ◽

10.3390/proceedings2019021022 ◽

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.

Download Full-text

Optimizing Answer Set Computation via Heuristic-Based Decomposition

Theory and Practice of Logic Programming ◽

10.1017/s1471068419000036 ◽

2019 ◽

Vol 19 (04) ◽

pp. 603-628 ◽

Cited By ~ 4

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.

Download Full-text

Inconsistency Proofs for ASP: The ASP - DRUPE Format

Theory and Practice of Logic Programming ◽

10.1017/s1471068419000255 ◽

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.

Download Full-text

Towards automated integration of guess and check programs in answer set programming: a meta-interpreter and applications

Theory and Practice of Logic Programming ◽

10.1017/s1471068405002577 ◽

2006 ◽

Vol 6 (1-2) ◽

pp. 23-60 ◽

Cited By ~ 12

Author(s):

THOMAS EITER ◽

AXEL POLLERES

Keyword(s):

Problem Solving ◽

Logic Program ◽

Answer Set Programming ◽

Polynomial Hierarchy ◽

Logic Programs ◽

Complete Problems ◽

Polynomial Size ◽

Disjunctive Logic Programs ◽

Np Complete ◽

Answer Set

Answer set programming (ASP) with disjunction offers a powerful tool for declaratively representing and solving hard problems. Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise and intuitive way, where the encoding reflects the typical “guess and check” nature of NP problems: The property is encoded in a way such that polynomial size certificates for it correspond to stable models of a program. However, the problem-solving capacity of full disjunctive logic programs (DLPs) is beyond NP, and captures a class of problems at the second level of the polynomial hierarchy. While these problems also have a clear “guess and check” structure, finding an encoding in a DLP reflecting this structure may sometimes be a non-obvious task, in particular if the “check” itself is a co-NP-complete problem; usually, such problems are solved by interleaving separate guess and check programs, where the check is expressed by inconsistency of the check program. In this paper, we present general transformations of head-cycle free (extended) disjunctive logic programs into stratified and positive (extended) disjunctive logic programs based on meta-interpretation techniques. The answer sets of the original and the transformed program are in simple correspondence, and, moreover, inconsistency of the original program is indicated by a designated answer set of the transformed program. Our transformations facilitate the integration of separate “guess” and “check” programs, which are often easy to obtain, automatically into a single disjunctive logic program. Our results complement recent results on meta-interpretation in ASP, and extend methods and techniques for a declarative “guess and check” problem solving paradigm through ASP.

Download Full-text

Temporal logic programs with variables

Theory and Practice of Logic Programming ◽

10.1017/s1471068416000570 ◽

2016 ◽

Vol 17 (2) ◽

pp. 226-243 ◽

Cited By ~ 1

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.

Download Full-text

Modeling and Language Extensions

AI Magazine ◽

10.1609/aimag.v37i3.2673 ◽

2016 ◽

Vol 37 (3) ◽

pp. 33-44 ◽

Cited By ~ 4

Author(s):

Martin Gebser ◽

Torsten Schaub

Keyword(s):

Expressive Language ◽

Logic Program ◽

Answer Set Programming ◽

Stable Model ◽

Logic Programs ◽

First Order ◽

High Level Modeling ◽

High Level ◽

Answer Sets ◽

First Order Variables

Answer set programming (ASP) has emerged as an approach to declarative problem solving based on the stable model semantics for logic programs. The basic idea is to represent a computational problem by a logic program, formulating constraints in terms of rules, such that its answer sets correspond to problem solutions. To this end, ASP combines an expressive language for high-level modeling with powerful low-level reasoning capacities, provided by off-the-shelf tools. Compact problem representations take advantage of genuine modeling features of ASP, including (first-order) variables, negation by default, and recursion. In this article, we demonstrate the ASP methodology on two example scenarios, illustrating basic as well as advanced modeling and solving concepts. We also discuss mechanisms to represent and implement extended kinds of preferences and optimization. An overview of further available extensions concludes the article.

Download Full-text

Automated Verification of Weak Equivalence within thesmodelsSystem

Theory and Practice of Logic Programming ◽

10.1017/s1471068407003031 ◽

2007 ◽

Vol 7 (6) ◽

pp. 697-744 ◽

Cited By ~ 7

Author(s):

TOMI JANHUNEN ◽

EMILIA OIKARINEN

Keyword(s):

Search Engine ◽

Logic Program ◽

General Setting ◽

Answer Set Programming ◽

Weak Equivalence ◽

Logic Programs ◽

Meta Level ◽

Level Problem ◽

Answer Sets ◽

Answer Set

AbstractIn answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using ananswer set solveras a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To ease answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programsPandQunder consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence ofPandQ. The method is developed here in a slightly more general setting by taking thevisibilityof atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator calledlpeqthat enables the verification of weak equivalence within thesmodelssystem using the same search engine as for the search of models. Our experiments withlpeqandsmodelssuggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.

Download Full-text