BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/492
DTSTAMP:20230914T125926Z
SUMMARY:Extensional Crisis and Proving Identity
DESCRIPTION:Speaker: Ashutosh Gupta (Institute of Science and Technology\nA
m campus 1\n3400 Klosterneuburg\nAustria)\n\nAbstract: \nAbstract: Extensi
onality axioms are common when reasoning about data collections\, such as
arrays and functions in program analysis\, or sets in mathematics. An exte
nsionality axiom asserts that two collections are equal if they consist of
the same elements at the same indices.\n\nUsing extensionality is often r
equired to show that two collections are equal. A typical example is the s
et theory theorem \\forall x)(\\forall y) x \\union y = y \\union x. Inter
estingly\, while humans have no problem with proving such set identities u
sing extensionality\, they are very hard for superposition theorem provers
because of the calculi they use.\n\nIn this work we show how addition of
a new inference rule\, called extensionality resolution\, allows first-ord
er theorem provers to easily solve problems no modern first-order theorem
prover can solve. We illustrate this by running the VAMPIRE theorem prover
with extensionality resolution on a number of set theory and array proble
ms. Extensionality resolution helps VAMPIRE to solve problems from the TPT
P library of first-order problems that were never solved before by any pro
ver.\n
URL:https://www.tcs.tifr.res.in/web/events/492
DTSTART;TZID=Asia/Kolkata:20140526T160000
DTEND;TZID=Asia/Kolkata:20140526T170000
LOCATION:D-405 (D-Block Seminar Room)
END:VEVENT
END:VCALENDAR