145
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
Manna and Pnueli have extensively shown how a mixture of first-order logic (FOL) and discrete Linear time Temporal Logic (LTL) is sufficient to precisely state verification problem...
119
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
Abstract. First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first...
130
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
Abstract. A method based on dependency pairs for showing termination of functional programs on data structures generated by constructors with relations is proposed. A functional pr...
89
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
We present a method for proving rigid first order theorems by encoding them as propositional satisfiability problems. We encode the existence of a first order connection tableau an...
67
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
103
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
Much research concerning Satisfiability Modulo Theories is devoted to the design of efficient SMT-solvers that integrate a SATsolver with T -satisfiability procedures. The rewrite-...
65
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
107
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
Abstract. In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equ...
76
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
76
Voted
CADE
2007
Springer
16 years 1 months ago
2007
Springer
