1 citations · 3 across the 3 of their papers we have counts for
4 papers
Complete Trigger Selection in Satisfiability modulo first-order Theories
Christopher Lynch, Stephen Miner
Let T be an SMT solver with no theory solvers except for Quantifier Instantiation. Given a set of first-order clauses S saturated by Resolution (with a valid literal selection func…
Congruence Closure Modulo Permutation Equations
Dohan Kim, Christopher Lynch
We present a framework for constructing congruence closure modulo permutation equations, which extends the abstract congruence closure framework for handling permutation function s…
On Asymmetric Unification for the Theory of XOR with a Homomorphism
Christopher Lynch, Andrew M. Marshall, Catherine Meadows +2
Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However,…
Bounded ACh Unification
Ajay Kumar Eeralla, Christopher Lynch
We consider the problem of the unification modulo an equational theory ACh, which consists of a function symbol that is homomorphic over an associative-commutative operator …