Automating the Search for Elegant Proofs
The TPTP Problem Library
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification
Automated Synthesis of Recursive Programs from a ∀∃ Logical Specification
Announcements