Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification Andrei Voronkov OriginalPaper Pages: 205 - 231
Automated Synthesis of Recursive Programs from a ∀∃ Logical Specification Jacques ChazarainSerge Muller OriginalPaper Pages: 233 - 275