Sciweavers

Share
LPAR
2010
Springer
9 years 6 months ago
Clause Elimination Procedures for CNF Formulas
Abstract. We develop and analyze clause elimination procedures, a specific family of simplification techniques for conjunctive normal form (CNF) formulas. Extending known procedu...
Marijn Heule, Matti Järvisalo, Armin Biere
LPAR
2010
Springer
9 years 6 months ago
How to Universally Close the Existential Rule
This paper introduces a nested sequent system for predicate logic. The system features a structural universal quantifier and a universally closed existential rule. One nice conseq...
Kai Brünnler
LPAR
2010
Springer
9 years 6 months ago
Aligators for Arrays (Tool Paper)
This paper presents Aligators, a tool for the generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic techniques to carry out i...
Thomas A. Henzinger, Thibaud Hottelier, Laura Kov&...
LPAR
2010
Springer
9 years 6 months ago
Lazy Abstraction for Size-Change Termination
traction for Size-Change Termination
Michael Codish, Carsten Fuhs, Jürgen Giesl, P...
LPAR
2010
Springer
9 years 6 months ago
PBINT, A Logic for Modelling Search Problems Involving Arithmetic
Shahab Tasharrofi, Eugenia Ternovska
books