Campus Event Calendar
Event Entry
What and Who
SMELS: Satisfiability Modulo Equality with Lazy Superposition
Duc-Khanh Tran
Max-Planck-Institut für Informatik - RG 1
Talk RG1 Group Meeting
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 9 November 2007
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
We give a method for extending efficient SMT solvers to handle
quantifiers, using Superposition inference rules. In our method,
the input formula is converted into CNF as in traditional first
order logic theorem provers. The ground clauses are given to
the SMT solver, which runs a DPLL method to build partial models.
The partial model is passed to a congruence closure procedure,
as is normally done in SMT. The congruence closure reduces the
partial model and passes it to a Superposition procedure, along
with a justification. The Superposition procedure then peforms
an inference rule, which we call Justified Superposition, between
the reduced partial model and the nonground clauses, plus usual
Superposition rules with the nonground clauses. Any resulting
ground clauses are provided to the DPLL engine. We prove the
completeness of this method, using a nontrivial modification of
the Bachmair Ganzinger model generation technique. We believe
this combination uses the best of both worlds, an SMT process
to handle ground clauses efficiently, and a Superposition
procedure which uses orderings to handle the nonground clauses.
An implementation based on these ideas is planned.
quantifiers, using Superposition inference rules. In our method,
the input formula is converted into CNF as in traditional first
order logic theorem provers. The ground clauses are given to
the SMT solver, which runs a DPLL method to build partial models.
The partial model is passed to a congruence closure procedure,
as is normally done in SMT. The congruence closure reduces the
partial model and passes it to a Superposition procedure, along
with a justification. The Superposition procedure then peforms
an inference rule, which we call Justified Superposition, between
the reduced partial model and the nonground clauses, plus usual
Superposition rules with the nonground clauses. Any resulting
ground clauses are provided to the DPLL engine. We prove the
completeness of this method, using a nontrivial modification of
the Bachmair Ganzinger model generation technique. We believe
this combination uses the best of both worlds, an SMT process
to handle ground clauses efficiently, and a Superposition
procedure which uses orderings to handle the nonground clauses.
An implementation based on these ideas is planned.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 11/05/2007 11:19
Roxane Wetzel, 10/24/2007 14:00 -- Created document.
Roxane Wetzel, 10/24/2007 14:00 -- Created document.