LPAR
2012
Springer
12 years 7 months ago
2012
Springer
E-matching is the most commonly used technique to handle quantifiers in SMT solvers. It works by identifying characteristic subexpressions of quantified formulae, named triggers,...
LPAR
2012
Springer
12 years 7 months ago
2012
Springer
We motivate and introduce a query language PrQL designed for inspecting machine representations of proofs. PrQL natively supports hiproofs which express proof structure using hiera...
LPAR
2012
Springer
12 years 7 months ago
2012
Springer
Abstract. The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has be...
LPAR
2012
Springer
12 years 7 months ago
2012
Springer
Abstract. We present a novel counterexample generator for the interactive theorem prover Isabelle based on a compiler that synthesizes test data generators for functional programmi...
LPAR
2012
Springer
12 years 7 months ago
2012
Springer
traction with Interpolants for Arrays Francesco Alberti1 , Roberto Bruttomesso2 , Silvio Ghilardi2 , Silvio Ranise3 , Natasha Sharygina1 1 Universit`a della Svizzera Italiana, Luga...