LPAR 2010 | Sciweavers

9

LPAR
2010
Springer

127views Automated Reasoning» more LPAR 2010»

Clause Elimination Procedures for CNF Formulas

13 years 3 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 »

14

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 3 months ago

Download lat.inf.tu-dresden.de

Franz Baader, Marcel Lippmann, Hongkai Liu

claim paper

Read More »

7

click to vote

LPAR
2010
Springer

121views Automated Reasoning» more LPAR 2010»

How to Universally Close the Existential Rule

13 years 3 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 »

16

click to vote

LPAR
2010
Springer

147views Automated Reasoning» more LPAR 2010»

Aligators for Arrays (Tool Paper)

13 years 3 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 »

13

click to vote

LPAR
2010
Springer

117views Automated Reasoning» more LPAR 2010»

Lazy Abstraction for Size-Change Termination

13 years 3 months ago

Download www.computational-logic.org

traction for Size-Change Termination

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