Home

Peter Schneider-Kamp

  1. Automated Termination Analysis for Logic Programs with Cut.

    Thu, 07/29/2010 - 15:01 — SomNambul
    Authors: Jürgen Giesl, Peter Schneider-Kamp, Thomas Ströder, Alexander Serebrenik, René Thiemann
    Subjects: Logic in Computer Science
    Abstract

    Termination is an important and well-studied property for logic programs.
    However, almost all approaches for automated termination analysis focus on
    definite logic programs, whereas real-world Prolog programs typically use the
    cut operator. We introduce a novel pre-processing method which automatically
    transforms Prolog programs into logic programs without cuts, where termination
    of the cut-free program implies termination of the original program. Hence
    after this pre-processing, any technique for proving termination of definite
    logic programs can be applied.

  2. Optimal Base Encodings for Pseudo-Boolean Constraints.

    Thu, 07/29/2010 - 15:01 — SomNambul
    Authors: Peter Schneider-Kamp, Michael Codish, Yoav Fekete, Carsten Fuhs
    Subjects: Discrete Mathematics
    Abstract

    This paper formalizes the "optimal base problem", presents an algorithm to
    solve it, and describes its application to the encoding of Pseudo-Boolean
    constraints to SAT. We demonstrate the impact of integrating our algorithm
    within the Pseudo-Boolean constraint solver MiniSAT+. Experimentation indicates
    that our algorithm scales to consider bases involving numbers up to 1,000,000,
    improving on the restriction in MiniSAT+ to prime numbers up to 17.

  3. Polytool: polynomial interpretations as a basis for termination analysis of Logic programs.

    Wed, 12/23/2009 - 16:01 — SomNambul
    Authors: Manh Thang Nguyen, Danny De Schreye, Jürgen Giesl, Peter Schneider-Kamp
    Subjects: Programming Languages
    Abstract

    Our goal is to study the feasibility of porting termination analysis
    techniques developed for one programming paradigm to another paradigm. In this
    paper, we show how to adapt termination analysis techniques based on polynomial
    interpretations - very well known in the context of term rewrite systems (TRSs)
    - to obtain new (non-transformational) ter- mination analysis techniques for
    definite logic programs (LPs). This leads to an approach that can be seen as a
    direct generalization of the traditional techniques in termination analysis of
    LPs, where linear norms and level mappings are used.

Math-arch

Syndicate content