Sciweavers

CADE
2007
Springer
14 years 3 months ago
An Incremental Technique for Automata-Based Decision Procedures
Abstract. Automata-based decision procedures commonly achieve optimal complexity bounds. However, in practice, they are often outperformed by sub-optimal (but more local-search bas...
David Toman, Gulay Ünel
CADE
2007
Springer
14 years 3 months ago
Logical Interpretation: Static Program Analysis Using Theorem Proving
Abstract. This paper presents the foundations for using automated deduction technology in static program analysis. The central principle is the use of logical lattices ? a class of...
Ashish Tiwari, Sumit Gulwani
CADE
2007
Springer
14 years 3 months ago
SRASS - A Semantic Relevance Axiom Selection System
This paper describes the design, implementation, and testing of a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a...
Geoff Sutcliffe, Yury Puzis
CADE
2007
Springer
14 years 3 months ago
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
We present an encoding that is able to specify LTL bounded model checking problems within the Bernays-Sch?onfinkel fragment of first-order logic. This fragment, which also correspo...
Andrei Voronkov, Juan Antonio Navarro Pérez
CADE
2007
Springer
14 years 3 months ago
Optimized Reasoning in Description Logics Using Hypertableaux
We present a novel reasoning calculus for Description Logics (DLs)--knowledge representation formalisms with applications in areas such as the Semantic Web. In order to reduce the ...
Boris Motik, Rob Shearer, Ian Horrocks
CADE
2007
Springer
14 years 3 months ago
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that combines 1) Boolean algebra of sets of uninterpreted elements (BA) and 2) Presburger arithmetic (PA). BA...
Viktor Kuncak, Martin C. Rinard
CADE
2007
Springer
14 years 3 months ago
System for Automated Deduction (SAD): A Tool for Proof Verification
In this paper, a proof assistant, called SAD, is presented. SAD deals with mathematical texts that are formalized in the ForTheL language (brief description of which is also given)...
Konstantin Verchinine, Alexander V. Lyaletski, And...
CADE
2007
Springer
14 years 3 months ago
Barendregt's Variable Convention in Rule Inductions
Abstract. Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt&#...
Christian Urban, Stefan Berghofer, Michael Norrish
CADE
2007
Springer
14 years 3 months ago
System Description: E-KRHyper
The E-KRHyper system is a model generator and theorem prover for first-order logic with equality. It implements the new E-hyper tableau calculus, which integrates a superposition-b...
Björn Pelzer, Christoph Wernhard