CADE
2007
Springer
14 years 12 months ago
2007
Springer
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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 ...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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)...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
Abstract. Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt&#...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
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...