LPAR 2010 | Sciweavers

30

LPAR
2010
Springer

127views Automated Reasoning» more LPAR 2010»

Clause Elimination Procedures for CNF Formulas

13 years 10 months ago

Abstract. We develop and analyze clause elimination procedures, a speciﬁc family of simpliﬁcation techniques for conjunctive normal form (CNF) formulas. Extending known procedu...

Marijn Heule, Matti Järvisalo, Armin Biere

claim paper

Read More »

32

click to vote

LPAR
2010
Springer

135views Automated Reasoning» more LPAR 2010»

Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics

13 years 10 months ago

Download lat.inf.tu-dresden.de

Franz Baader, Marcel Lippmann, Hongkai Liu

claim paper

Read More »

30

click to vote

LPAR
2010
Springer

121views Automated Reasoning» more LPAR 2010»

How to Universally Close the Existential Rule

13 years 10 months ago

Download www.iam.unibe.ch

This paper introduces a nested sequent system for predicate logic. The system features a structural universal quantiﬁer and a universally closed existential rule. One nice conseq...

Kai Brünnler

claim paper

Read More »

41

click to vote

LPAR
2010
Springer

147views Automated Reasoning» more LPAR 2010»

Aligators for Arrays (Tool Paper)

13 years 10 months ago

Download www.complang.tuwien.ac.at

This paper presents Aligators, a tool for the generation of universally quantiﬁed array invariants. Aligators leverages recurrence solving and algebraic techniques to carry out i...

Thomas A. Henzinger, Thibaud Hottelier, Laura Kov&...

claim paper

Read More »

31

click to vote

LPAR
2010
Springer

117views Automated Reasoning» more LPAR 2010»

Lazy Abstraction for Size-Change Termination

13 years 10 months ago

Download www.computational-logic.org

traction for Size-Change Termination

Michael Codish, Carsten Fuhs, Jürgen Giesl, P...