An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

Grounding and Solving in Answer Set Programming

AI Magazine ◽

10.1609/aimag.v37i3.2672 ◽

2016 ◽

Vol 37 (3) ◽

pp. 25-32 ◽

Cited By ~ 27

Author(s):

Benjamin Kaufmann ◽

Nicola Leone ◽

Simona Perri ◽

Torsten Schaub

Keyword(s):

Problem Solving ◽

Propositional Logic ◽

Logic Program ◽

Answer Set Programming ◽

Key Issues ◽

Answer Sets ◽

Answer set programming is a declarative problem solving paradigm that rests upon a workflow involving modeling, grounding, and solving. While the former is described by Gebser and Schaub (2016), we focus here on key issues in grounding, or how to systematically replace object variables by ground terms in a effective way, and solving, or how to compute the answer sets of a propositional logic program obtained by grounding.

Here and There with Arithmetic

10.1017/s1471068421000338 ◽

2021 ◽

pp. 1-15

Author(s):

VLADIMIR LIFSCHITZ

Keyword(s):

Programming Language ◽

Propositional Logic ◽

Answer Set Programming ◽

The Other ◽

Arithmetic Operations ◽

First Order ◽

The Relationship ◽

Abstarct In the theory of answer set programming, two groups of rules are called strongly equivalent if, informally speaking, they have the same meaning in any context. The relationship between strong equivalence and the propositional logic of here-and-there allows us to establish strong equivalence by deriving rules of each group from rules of the other. In the process, rules are rewritten as propositional formulas. We extend this method of proving strong equivalence to an answer set programming language that includes operations on integers. The formula representing a rule in this language is a first-order formula that may contain comparison symbols among its predicate constants, and symbols for arithmetic operations among its function constants. The paper is under consideration for acceptance in TPLP.

Proving infinitary formulas

10.1017/s1471068416000302 ◽

2016 ◽

Vol 16 (5-6) ◽

pp. 787-799 ◽

Cited By ~ 1

Author(s):

AMELIA HARRISON ◽

VLADIMIR LIFSCHITZ ◽

JULIAN MICHAEL

Keyword(s):

Propositional Logic ◽

Formal System ◽

Answer Set Programming ◽

Logic Programs ◽

Deductive Systems ◽

AbstractThe infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas.

Applications of intuitionistic logic in Answer Set Programming

10.1017/s1471068403001881 ◽

2004 ◽

Vol 4 (3) ◽

pp. 325-354 ◽

Cited By ~ 20

Author(s):

MAURICIO OSORIO ◽

JUAN A. NAVARRO ◽

JOSÉ ARRAZOLA

Keyword(s):

Declarative encodings of acyclicity properties

Journal of Logic and Computation ◽

10.1093/logcom/exv063 ◽

2015 ◽

Vol 30 (4) ◽

pp. 923-952

Author(s):

Martin Gebser ◽

Tomi Janhunen ◽

Jussi Rintanen

Keyword(s):

Linear Programming ◽

Knowledge Representation ◽

Structural Properties ◽

Propositional Logic ◽

Answer Set Programming ◽

Tree Structures ◽

Computational Performance ◽

Primary Representation ◽

Representation Language ◽

Abstract Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such structural properties is non-obvious and can be challenging indeed. In this article, we take a number of acyclicity properties into consideration and investigate various logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic and linear programming. We study the compactness of encodings and the resulting computational performance on benchmarks involving acyclic or tree structures.

Transition systems for model generators—A unifying approach

10.1017/s1471068411000214 ◽

2011 ◽

Vol 11 (4-5) ◽

pp. 629-646 ◽

Cited By ~ 8

Author(s):

YULIYA LIERLER ◽

MIROSLAW TRUSZCZYNSKI

Keyword(s):

Logic Programming ◽

Propositional Logic ◽

Answer Set Programming ◽

Transition Systems ◽

Satisfiability Solvers ◽

Answer Set Semantics ◽

Computing Models ◽

AbstractA fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as “satisfiability modulo answer-set programming,” where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).