scholarly journals Stable-unstable semantics: Beyond NP with normal logic programs

2016 ◽  
Vol 16 (5-6) ◽  
pp. 570-586 ◽  
Author(s):  
BART BOGAERTS ◽  
TOMI JANHUNEN ◽  
SHAHAB TASHARROFI
Keyword(s):  
Logic Programming ◽  
Logic Programs ◽  
New Paradigm ◽  
Search Problems ◽  
Quantified Boolean Formulas ◽  
Disjunctive Logic Programs ◽  
Boolean Formulas ◽  
Normal Logic ◽  
The Rich ◽  
High Level

AbstractStandard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophisticated techniques such as saturation or meta-interpretation. The application of such techniques easily leads to encodings that are inaccessible to non-experts. Furthermore, while disjunctive ASP solvers often rely on calls to a (co-)NP oracle, it may be difficult to detect from the input program where the oracle is being accessed. In other formalisms, such as Quantified Boolean Formulas (QBFs), the interface to the underlying oracle is more transparent as it is explicitly recorded in the quantifier prefix of a formula. On the other hand, ASP has advantages over QBFs from the modeling perspective. The rich high-level languages such as ASP-Core-2 offer a wide variety of primitives that enable concise and natural encodings of search problems. In this paper, we present a novel logic programming–based modeling paradigm that combines the best features of ASP and QBFs. We develop so-calledcombined logic programsin which oracles are directly cast as (normal) logic programs themselves. Recursive incarnations of this construction enable logic programming on arbitrarily high levels of the PH. We develop a proof-of-concept implementation for our new paradigm.

scholarly journals Generating Hard Random Boolean Formulas and Disjunctive Logic Programs

2017 ◽  
Author(s):  
Giovanni Amendola ◽  
Francesco Ricca ◽  
Miroslaw Truszczynski
Keyword(s):  
Phase Transition ◽  
Transition Region ◽  
Real World ◽  
Logic Program ◽  
Logic Programs ◽  
Quantified Boolean Formulas ◽  
Disjunctive Logic Programs ◽  
Boolean Formulas ◽  
Phase Transition Region ◽  
Standard Models

We propose a model of random quantified boolean formulas and their natural random disjunctive logic program counterparts. The model extends the standard models for random SAT and 2QBF. We provide theoretical bounds for the phase transition region in the new model, and show experimentally the presence of the easy-hard-easy pattern. Importantly, we show that the model is well suited for assessing solvers tuned to real-world instances. Moreover, to the best of our knowledge, our model and results on random disjunctive logic programs are the first of their kind.

scholarly journals Interdefinability of defeasible logic and logic programming under the well-founded semantics

2011 ◽  
Vol 13 (1) ◽  
pp. 107-142 ◽  
Author(s):  
FREDERICK MAIER
Keyword(s):  
Logic Programming ◽  
Opposite Direction ◽  
Stable Model ◽  
Logic Programs ◽  
Defeasible Logic ◽  
Normal Logic

AbstractWe provide a method of translating theories of Nute's defeasible logic into logic programs, and a corresponding translation in the opposite direction. Under certain natural restrictions, the conclusions of defeasible theories under the ambiguity propagating defeasible logic ADL correspond to those of the well-founded semantics for normal logic programs, and so it turns out that the two formalisms are closely related. Using the same translation of logic programs into defeasible theories, the semantics for the ambiguity blocking defeasible logic NDL can be seen as indirectly providing an ambiguity blocking semantics for logic programs. We also provide antimonotone operators for both ADL and NDL, each based on the Gelfond–Lifschitz (GL) operator for logic programs. For defeasible theories without defeaters or priorities on rules, the operator for ADL corresponds to the GL operator and so can be seen as partially capturing the consequences according to ADL. Similarly, the operator for NDL captures the consequences according to NDL, though in this case no restrictions on theories apply. Both operators can be used to define stable model semantics for defeasible theories.

scholarly journals Characterising equilibrium logic and nested logic programs: Reductions and complexity,

2009 ◽  
Vol 9 (05) ◽  
pp. 565-616 ◽  
Author(s):  
DAVID PEARCE ◽  
HANS TOMPITS ◽  
STEFAN WOLTRAN
Keyword(s):  
Propositional Logic ◽  
Stable Model ◽  
Logic Programs ◽  
Complexity Bounds ◽  
Inference Engines ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Reasoning Tasks ◽  
Answer Set Semantics ◽  
Quantified Propositional Logic

AbstractEquilibrium logic is an approach to non-monotonic reasoning that extends the stable-model and answer-set semantics for logic programs. In particular, it includes the general case ofnested logic programs, where arbitrary Boolean combinations are permitted in heads and bodies of rules, as special kinds of theories. In this paper, we present polynomial reductions of the main reasoning tasks associated with equilibrium logic and nested logic programs intoquantified propositional logic, an extension of classical propositional logic where quantifications over atomic formulas are permitted. Thus, quantified propositional logic is a fragment of second-order logic, and its formulas are usually referred to asquantified Boolean formulas(QBFs). We provide reductions not only for decision problems, but also for the central semantical concepts of equilibrium logic and nested logic programs. In particular, our encodings map a given decision problem into some QBF such that the latter is valid precisely in case the former holds. The basic tasks we deal with here are theconsistency problem,brave reasoningandskeptical reasoning. Additionally, we also provide encodings for testing equivalence of theories or programs under different notions of equivalence, viz.ordinary,stronganduniform equivalence. For all considered reasoning tasks, we analyse their computational complexity and give strict complexity bounds. Hereby, our encodings yield upper bounds in a direct manner. Besides this useful feature, our approach has the following benefits: First, our encodings yield auniform axiomatisationfor a variety of problems in a common language. Second, extant solvers for QBFs can be used as back-end inference engines to realise implementations of the encoded task in a rapid prototyping manner. Third, our axiomatisations also allow us to straightforwardly relate equilibrium logic with circumscription.

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 Semantics for Possibilistic Disjunctive Programs

2011 ◽  
Vol 13 (1) ◽  
pp. 33-70 ◽  
Author(s):  
JUAN CARLOS NIEVES ◽  
MAURICIO OSORIO ◽  
ULISES CORTÉS
Keyword(s):  
Logic Programming ◽  
Knowledge Base ◽  
Logic Program ◽  
Programming Approach ◽  
Logic Programs ◽  
Possibilistic Logic ◽  
Point Operator ◽  
Disjunctive Logic Programs ◽  
Answer Sets ◽  
Disjunctive Programs

AbstractIn this paper, a possibilistic disjunctive logic programming approach for modeling uncertain, incomplete, and inconsistent information is defined. This approach introduces the use of possibilistic disjunctive clauses, which are able to capture incomplete information and states of a knowledge base at the same time. By considering a possibilistic logic program as a possibilistic logic theory, a construction of a possibilistic logic programming semantic based on answer sets and the proof theory of possibilistic logic is defined. It shows that this possibilistic semantics for disjunctive logic programs can be characterized by a fixed-point operator. It is also shown that the suggested possibilistic semantics can be computed by a resolution algorithm and the consideration of optimal refutations from a possibilistic logic theory. In order to manage inconsistent possibilistic logic programs, a preference criterion between inconsistent possibilistic models is defined. In addition, the approach of cuts for restoring consistency of an inconsistent possibilistic knowledge base is adopted. The approach is illustrated in a medical scenario.

scholarly journals New models for generating hard random boolean formulas and disjunctive logic programs

2020 ◽  
Vol 279 ◽  
pp. 103185 ◽  
Author(s):  
Giovanni Amendola ◽  
Francesco Ricca ◽  
Miroslaw Truszczynski
Keyword(s):  
Logic Programs ◽  
New Models ◽  
Disjunctive Logic Programs ◽  
Boolean Formulas

scholarly journals Logical English meets legal English for swaps and derivatives

2021 ◽  
Author(s):  
Robert Kowalski ◽  
Akber Datoo
Keyword(s):  
Logic Programming ◽  
Standard Form ◽  
English Speakers ◽  
Logic Programs ◽  
Basic Form ◽  
Computer Languages ◽  
Legal Documents ◽  
Controlled Natural Language ◽  
Normal Logic ◽  
Conventional Computer

AbstractIn this paper, we present an informal introduction to Logical English (LE) and illustrate its use to standardise the legal wording of the Automatic Early Termination (AET) clauses of International Swaps and Derivatives Association (ISDA) Agreements. LE can be viewed both as an alternative to conventional legal English for expressing legal documents, and as an alternative to conventional computer languages for automating legal documents. LE is a controlled natural language (CNL), which is designed both to be computer-executable and to be readable by English speakers without special training. The basic form of LE is syntactic sugar for logic programs, in which all sentences have the same standard form, either as rules of the form conclusion if conditions or as unconditional sentences of the form conclusion. However, LE extends normal logic programming by introducing features that are present in other computer languages and other logics. These features include typed variables signalled by common nouns, and existentially quantified variables in the conclusions of sentences signalled by indefinite articles. Although LE translates naturally into a logic programming language such as Prolog or ASP, it can also serve as a neutral standard, which can be compiled into other lower-level computer languages.

scholarly journals Performing fully parallel constraint logic programming on a quantum annealer

2018 ◽  
Vol 18 (5-6) ◽  
pp. 928-949 ◽  
Author(s):  
SCOTT PAKIN
Keyword(s):  
Logic Programming ◽  
Constraint Logic Programming ◽  
Logic Programs ◽  
Machine Model ◽  
Computing Systems ◽  
Model Hamiltonian ◽  
Constraint Logic Programs ◽  
Classical Computing ◽  
Specialized Hardware ◽  
High Level

AbstractAquantum annealerexploits quantum effects to solve a particular type of optimization problem. The advantage of this specialized hardware is that it effectively considers all possible solutions in parallel, thereby potentially outperforming classical computing systems. However, despite quantum annealers having recently become commercially available, there are relatively few high-level programming models that target these devices. In this article, we show how to compile a subset of Prolog enhanced with support for constraint logic programming into a two-local Ising-model Hamiltonian suitable for execution on a quantum annealer. In particular, we describe the series of transformations one can apply to convert constraint logic programs expressed in Prolog into an executable form that bears virtually no resemblance to a classical machine model yet that evaluates the specified constraints in a fully parallel manner. We evaluate our efforts on a 1,095-qubit D-Wave 2X quantum annealer and describe the approach's associated capabilities and shortcomings.

scholarly journals Deriving conclusions from non-monotonic cause-effect relations

2016 ◽  
Vol 16 (5-6) ◽  
pp. 670-687 ◽  
Author(s):  
JORGE FANDINNO
Keyword(s):  
Knowledge Representation ◽  
Logic Programming ◽  
Causal Effect ◽  
Stable Model ◽  
Logic Programs ◽  
Causal Relations ◽  
Initial Approach ◽  
Sufficient Cause ◽  
Different Types ◽  
Normal Logic

AbstractWe present an extension of Logic Programming (under stable models semantics) that, not only allows concluding whether a true atom is a cause of another atom, but alsoderiving new conclusionsfrom these causal-effect relations. This is expressive enough to capture informal rules like “if some agent's actionshave beennecessaryto cause an eventEthen conclude atomcaused(,E),” something that, to the best of our knowledge, had not been formalised in the literature. To this aim, we start from a first attempt that proposed extending the syntax of logic programs with so-calledcausal literals. These causal literals are expressions that can be used in rule bodies and allow inspecting the derivation of some atomAin the program with respect to some query function ψ. Depending on how these query functions are defined, we can model different types of causal relations such as sufficient, necessary or contributory causes, for instance. The initial approach was specifically focused on monotonic query functions. This was enough to cover sufficient cause-effect relations but, unfortunately, necessary and contributory are essentiallynon-monotonic. In this work, we define a semantics for non-monotonic causal literals showing that, not only extends the stable model semantics for normal logic programs, but also preserves many of its usual desirable properties for the extended syntax. Using this new semantics, we provide precise definitions ofnecessaryandcontributorycausal relations and briefly explain their behaviour on a pair of typical examples from the Knowledge Representation literature.

scholarly journals Logic programs with monotone abstract constraint atoms

2008 ◽  
Vol 8 (2) ◽  
pp. 167-199 ◽  
Author(s):  
VICTOR W. MAREK ◽  
ILKKA NIEMELÄ ◽  
MIROSŁAW TRUSZCZYŃSKI
Keyword(s):  
Logic Programming ◽  
Logic Programs ◽  
Common Generalization ◽  
One Step ◽  
Normal Logic ◽  
The One ◽  
Operational Concept ◽  
Stable Models

AbstractWe introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atoms lparse programs) with the semantics of stable models, as defined by Niemelä, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue.

Sign in / Sign up

Export Citation Format

Share Document