Author name cluster

Johan Wittocx

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

JELIA Conference 2010 Conference Paper

An Approximative Inference Method for Solving THERE EXISTS FOR ALL SO Satisfiability Problems

Hanne Vlaeminck
Johan Wittocx
Joost Vennekens
Marc Denecker
Maurice Bruynooghe

Abstract The fragment ∃ ∀ SO ( ID ) of second order logic extended with inductive definitions is expressive, and many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard ( \(\Sigma^P_2\) ). In this paper, we develop an approximate, sound but incomplete method for solving such problems that transforms a ∃ ∀ SO ( ID ) to a ∃ SO ( ID ) problem. The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. We show that this provides an effective method for solving practically useful problems, such as common examples of conformant planning. We also propose a more complete translation to ∃ SO ( FP ), existential SO extended with nested inductive and coinductive definitions.

Details

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.

AAAI Conference 2008 Conference Paper

Grounding with Bounds

Johan Wittocx

Grounding is the task of reducing a first-order theory to an equivalent propositional one. Typical grounders work on a sentence-by-sentence level, substituting variables by domain elements and simplifying where possible. In this work, we propose a method for reasoning on the first-order theory as a whole to optimize the grounding process. Concretely, we develop an algorithm that computes bounds for subformulas. Such bounds indicate for which tuples the subformulas are certainly true and for which they are certainly false. These bounds can then be used by standard grounding algorithms to substantially reduce grounding sizes, and consequently also grounding times. We have implemented the method, and demonstrate its practical applicability.

PDF Details

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