BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Automated Theorem Proving with Equality Matching
DTSTART:20121026T140000
DTEND:20121026T150000
DTSTAMP:20260410T125200Z
UID:c921c79edc119c1ad5f082d0b179406d6288abb98acc7f6b7bf743e0
CATEGORIES:Conferences - Seminars
DESCRIPTION:Philipp Rümmer\nE-matching is the most commonly used techniqu
 e to handle quantifiers\nin Satisfiability Modulo Theory solvers. It works
  by identifying characteristic\nsub-expressions of quantified formulae\, n
 amed triggers\, which are\nmatched during proof search on ground terms to 
 discover relevant\ninstantiations of the quantified formula. E-matching ha
 s proven to\nbe an efficient and practical approach to handle quantifiers\
 , in\nparticular because triggers can be provided by the user to guide\npr
 oof search\; however\, as it is heuristic in nature\, e-matching\nalone is
  typically insufficient to establish a complete proof\nprocedure. In contr
 ast\, free variable methods in tableau-like\ncalculi are more robust and g
 ive rise to complete procedures\, e.g.\,\nfor first-order logic\, but are 
 not comparable to e-matching in terms\nof scalability. This paper discusse
 s how e-matching can be combined\nwith free variable approaches\, leading 
 to calculi that enjoy similar\ncompleteness properties as pure free variab
 le procedures\, but in\nwhich it is still possible for a user to provide d
 omain-specific\ntriggers to improve performance.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR