E-unification with constants vs. general E-unification. (English)

Dealing with satisfiability and n-ary CSPs in a logical framework. (English)

An instantiation scheme for satisfiability modulo theories. (English)

SAT modulo linear arithmetic for solving polynomial constraints. (English)

A decidability result for the model checking of infinite-state systems. (English)

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. (English)

Decidability and combination results for two notions of knowledge in security protocols. (English)

The area method. A recapitulation. (English)

Proof pearl: a formal proof of Dally and Seitz’ necessary and sufficient condition for deadlock-free routing in interconnection networks. (English)

Unification modulo homomorphic encryption. (English)

Computing knowledge in security protocols under convergent equational theories. (English)

Decidability of equivalence of symbolic derivations. (English)

State and progress in strand spaces: proving fair exchange. (English)

Reducing equational theories for the decision of static equivalence. (English)

Classical logic with partial functions. (English)

Tractable extensions of the description logic ${\mathcal{EL}}$ with numerical datatypes. (English)

Decreasing diagrams and relative termination. (English)

Analytic tableaux for higher-order logic with choice. (English)

Monotonicity inference for higher-order formulas. (English)

An interpolating sequent calculus for quantifier-free Presburger arithmetic. (English)