Automated Theorem Proving with Equality Matching
Event details
| Date | 26.10.2012 |
| Hour | 14:00 › 15:00 |
| Speaker | Philipp Rümmer |
| Location | |
| Category | Conferences - Seminars |
E-matching is the most commonly used technique to handle quantifiers
in Satisfiability Modulo Theory solvers. It works by identifying characteristic
sub-expressions of quantified formulae, named triggers, which are
matched during proof search on ground terms to discover relevant
instantiations of the quantified formula. E-matching has proven to
be an efficient and practical approach to handle quantifiers, in
particular because triggers can be provided by the user to guide
proof search; however, as it is heuristic in nature, e-matching
alone is typically insufficient to establish a complete proof
procedure. In contrast, free variable methods in tableau-like
calculi are more robust and give rise to complete procedures, e.g.,
for first-order logic, but are not comparable to e-matching in terms
of scalability. This paper discusses how e-matching can be combined
with free variable approaches, leading to calculi that enjoy similar
completeness properties as pure free variable procedures, but in
which it is still possible for a user to provide domain-specific
triggers to improve performance.
in Satisfiability Modulo Theory solvers. It works by identifying characteristic
sub-expressions of quantified formulae, named triggers, which are
matched during proof search on ground terms to discover relevant
instantiations of the quantified formula. E-matching has proven to
be an efficient and practical approach to handle quantifiers, in
particular because triggers can be provided by the user to guide
proof search; however, as it is heuristic in nature, e-matching
alone is typically insufficient to establish a complete proof
procedure. In contrast, free variable methods in tableau-like
calculi are more robust and give rise to complete procedures, e.g.,
for first-order logic, but are not comparable to e-matching in terms
of scalability. This paper discusses how e-matching can be combined
with free variable approaches, leading to calculi that enjoy similar
completeness properties as pure free variable procedures, but in
which it is still possible for a user to provide domain-specific
triggers to improve performance.
Practical information
- Informed public
- Free
Organizer
- Viktor Kuncak
Contact
- Viktor Kuncak