Using model generation theorem provers for the computation of answer sets

Download

index.pdf

Date

2009

Author

Sabuncu, Orkunt

Metadata

Show full item record

Item Usage Stats

242
views

61
downloads

Answer set programming (ASP) is a declarative approach to solving search problems. Logic programming constitutes the foundation of ASP. ASP is not a proof-theoretical approach where you get solutions by answer substitutions. Instead, the problem is represented by a logic program in such a way that models of the program according to the answer set semantics correspond to solutions of the problem. Answer set solvers (Smodels, Cmodels, Clasp, and Dlv) are used for finding answer sets of a given program. Although users can write programs with variables for convenience, current answer set solvers work on ground logic programs where there are no variables. The grounding step of ASP generates a propositional instance of a logic program with variables. It may generate a huge propositional instance and make the search process of answer set solvers more difficult. Model generation theorem provers (Paradox, Darwin, and FM-Darwin) have the capability of producing a model when the first-order input theory is satisfiable. This work proposes the use of model generation theorem provers as computational engines for ASP. The main motivation is to eliminate the grounding step of ASP completely or to perform it more intelligently using the model generation system. Additionally, regardless of grounding, model generation systems may display better performance than the current solvers. The proposed method can be seen as lifting SAT-based ASP, where SAT solvers are used to compute answer sets, to the first-order level for tight programs. A completion procedure which transforms a logic program to formulas of first-order logic is utilized. Besides completion, other transformations which are necessary for forming a firstorder theory suitable for model generation theorem provers are investigated. A system called Completor is implemented for handling all the necessary transformations. The empirical results demonstrate that the use of Completor and the theorem provers together can be an e ective way of computing answer sets. Especially, the run time results of Paradox in the experiments has showed that using Completor and Paradox together is favorable compared to answer set solvers. This advantage has been more clearly observed for programs with large propositional instances, since grounding can be a bottleneck for such programs.

Subject Keywords

Bioinformatics., Mathematical methods and modelling

URI

http://etd.lib.metu.edu.tr/upload/12610705/index.pdf
https://hdl.handle.net/11511/18753

Collections

Graduate School of Natural and Applied Sciences, Thesis

Suggestions

OpenMETU
Core

Using Criticalities as a Heuristic for Answer Set Programming SABUNCU, ORKUNT; Alpaslan, Ferda Nur; AKMAN, VAROL (2004-01-08) Answer Set Programming is a new paradigm based on logic programming. The main component of answer set programming is a system that finds the answer sets of logic programs. During the computation of an answer set, systems are faced with choice points where they have to select a literal and assign it a truth value. Generally, systems utilize some heuristics to choose new literals at the choice points. The heuristic used is one of the key factors for the performance of the system. A new heuristic for answer s...
Multi-objective integer programming: A general approach for generating all non-dominated solutions Oezlen, Melih; Azizoğlu, Meral (Elsevier BV, 2009-11-16) In this paper we develop a general approach to generate all non-dominated solutions of the multi-objective integer programming (MOIP) Problem. Our approach, which is based on the identification of objective efficiency ranges, is an improvement over classical epsilon-constraint method. Objective efficiency ranges are identified by solving simpler MOIP problems with fewer objectives. We first provide the classical epsilon-constraint method on the bi-objective integer programming problem for the sake of comple...
Using chains of bottleneck transitions to decompose and solve reinforcement learning tasks with hidden states Aydın, Hüseyin; Çilden, Erkin; Polat, Faruk (2022-08-01) Reinforcement learning is known to underperform in large and ambiguous problem domains under partial observability. In such cases, a proper decomposition of the task can improve and accelerate the learning process. Even ambiguous and complex problems that are not solvable by conventional methods turn out to be easier to handle by using a convenient problem decomposition, followed by the incorporation of machine learning methods for the sub-problems. Like in most real-life problems, the decomposition of a ta...
On Verification of Restricted Extended Affine Equivalence of Vectorial Boolean Functions Özbudak, Ferruh; Yayla, Oğuz (2015-02-01) Vectorial Boolean functions are used as substitution boxes in cryptosystems. Designing inequivalent functions resistant to known attacks is one of the challenges in cryptography. In doing this, finding a fast technique for determining whether two given functions are equivalent is a significant problem. A special class of the equivalence called restricted extended affine (REA) equivalence is studied in this paper. We update the verification procedures of the REA-equivalence types given in the recent work of ...
Using object-oriented materialized views to answer selection-based complex queries Alhajj, R; Polat, Faruk (1999-09-01) Presented in this paper is a model that utilizes existing materialized views to handle a wide range of complex selection-based queries, including linear recursive queries. Such queries are complex because it is almost impossible for naive users to predict the formulation of their predicate expressions. Object variables bound to objects in the result of a query are allowed to appear in the predicate of that query. Also, the predicate definition is extended to make it possible to have in the output only a sub...

Citation Formats

O. Sabuncu, “Using model generation theorem provers for the computation of answer sets,” Ph.D. - Doctoral Program, Middle East Technical University, 2009.