Sava Krstic, Albert Oliveras
Proceedings of the Fifth International Workshop on Satisfiability Modulo Theories
SMT-2007, 2008.

@proceedings{SMT-2007,
	address       = "Berlin, Germany",
	editor        = "Sava Krstic and Albert Oliveras",
	journal       = "{Electronic Notes in Theoretical Computer Science}",
	number        = 2,
	title         = "{Proceedings of the Fifth International Workshop on Satisfiability Modulo Theories}",
	volume        = 198,
	year          = 2008,
}

Event page: http://www.cs.upc.edu/~oliveras/smt07/home.html

Contents (5 items)

SMT-2007-RozanovS08 #constraints #generative #logic #similarity #transitive

Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic (MR, OS), pp. 3–17.

SMT-2007-MoskalLK08

E-matching for Fun and Profit (MM, JL, JRK), pp. 19–35.

SMT-2007-MouraB08 #modelling

Model-based Theory Combination (LMdM, NB), pp. 37–49.

SMT-2007-ConchonCKL08 #congruence #semantics

CC(X): Semantic Combination of Congruence Closure with Solvable Theories (SC, EC, JK, SL), pp. 51–69.

SMT-2007-BongioKLLM08 #encoding #first-order #proving #smt

Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.