Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Skolemization Modulo Theories

Konstantin Korovin and Margus Veanes

Abstract

Combining classical automated theorem proving techniques with theory based reasoning, such as satisfiability modulo theories, is a new approach to first-order reasoning modulo theories. Skolemization is a classical technique used to transform first-order formulas into equisatisfiable form. We show how Skolemization can benefit from a new satisfiability modulo theories based simplification technique of formulas called monadic decomposition. The technique can be used to transform a theory dependent formula over multiple variables into an equivalent form as a Boolean combination of unary formulas, where a unary formula depends on a single variable. In this way, theory specific variable dependencies can be eliminated and consequently, Skolemization can be refined by minimizing variable scopes in the decomposed formula in order to yield simpler Skolem terms.

Details

Publication typeInproceedings
Published inICMS'14
URLhttp://www.springerprofessional.de/047---skolemization-modulo-theories/5245762.html
Pages303-306
Volume8592
SeriesLNCS
PublisherSpringer
> Publications > Skolemization Modulo Theories