Author name cluster

Maarten Mariën

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

KR Conference 2008 Conference Paper

Approximate Reasoning in First-Order Logic Theories

Johan Wittocx
Maarten Mariën
Marc Denecker

Many computational settings are concerned with finding (all) models of a first-order logic theory for a fixed, finite domain. In this paper, we present a method to compute from a given theory and finite domain an approximate structure: a structure that approximates all models. We show confluence of this method and investigate its complexity. We discuss some applications, including 3-valued query answering in integrated and partially incomplete databases, and improved grounding in the context of model expansion for first-order logic.

SAT Conference 2008 Conference Paper

SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions

Maarten Mariën
Johan Wittocx
Marc Denecker
Maurice Bruynooghe

Abstract We investigate the satisfiability problem, SAT(ID), of an extension of propositional logic with inductive definitions. We demonstrate how to extend existing SAT solvers to become SAT(ID) solvers, and provide an implementation on top of MiniSat. We also report on a performance study, in which our implementation exhibits the expected benefits: full use of the underlying SAT solver’s potential.

Details

LPAR Conference 2007 Conference Paper

Integrating Inductive Definitions in SAT

Maarten Mariën
Johan Wittocx
Marc Denecker

Abstract We investigate techniques for supporting inductive definitions (IDs) in SAT, and report on an implementation, called MidL, of the resulting solver. This solver was first introduced in [11], as a part of a declarative problem solving framework. We go about our investigation by proposing a new formulation of the semantics of IDs as presented in [2]. This new formulation suggests a way to perform the computational task involved, resulting in an algorithm supporting IDs. We show in detail how to integrate our algorithm with traditional SAT solving techniques. We also point out the similarities with another algorithm that was recently developed for ASP [1]. Indeed, our formulation reveals a very tight relation with stable model semantics. We conclude by an experimental validation of our approach using MidL.

Details

LPAR Conference 2005 Conference Paper

Satisfiability Checking for PC(ID)

Maarten Mariën
Rudradeb Mitra
Marc Denecker
Maurice Bruynooghe

Abstract The logic FO(ID) extends classical first order logic with inductive definitions. This paper studies the satisifiability problem for PC(ID), its propositional fragment. We develop a framework for model generation in this logic, present an algorithm and prove its correctness. As FO(ID) is an integration of classical logic and logic programming, our algorithm integrates techniques from SAT and ASP. We report on a prototype system, called M id L, experimentally validating our approach.

Details

JELIA Conference 2004 Conference Paper

On the Relation Between ID-Logic and Answer Set Programming

Maarten Mariën
David Gilis
Marc Denecker

Abstract This paper is an analysis of two knowledge representation extensions of logic programming, namely Answer Set Programming and ID-Logic. Our aim is to compare both logics on the level of declarative reading, practical methodology and formal semantics. At the level of methodology, we put forward the thesis that in many (but not all) existing applications of ASP, an ASP program is used to encode definitions and assertions, similar as in ID-Logic. We illustrate this thesis with an example and present a formal result that supports it, namely an equivalence preserving translation from a class of ID-Logic theories into ASP. This translation can be exploited also to use the current efficient ASP solvers to reason on ID-Logic theories and it has been used to implement a model generator for ID-Logic.

Details