140
Voted
CADE
2007
Springer
16 years 29 days 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...
115
Voted
CADE
2007
Springer
16 years 29 days 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...
125
Voted
CADE
2007
Springer
16 years 29 days 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...
85
Voted
CADE
2007
Springer
16 years 29 days 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...
63
Voted
CADE
2007
Springer
16 years 29 days ago
2007
Springer
98
Voted
CADE
2007
Springer
16 years 29 days 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-...
62
Voted
CADE
2007
Springer
16 years 29 days ago
2007
Springer
99
Voted
CADE
2007
Springer
16 years 29 days 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...
74
Voted
CADE
2007
Springer
16 years 29 days ago
2007
Springer
75
Voted
CADE
2007
Springer
16 years 29 days ago
2007
Springer
