2 citations · 4 across the 5 of their papers we have counts for
5 papers
A new introduction rule for disjunction
Alejandro Díaz-Caro, Gilles Dowek
We extend Natural Deduction for intuitionistic logic with a third introduction rule for the disjunction, -i3, with a conclusion , but both premises $Γ\vdash…
A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
Gilles Dowek
We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on t…
A linear proof language for second-order intuitionistic linear logic
Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky +1
We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling…
Automatic Proof Checking and Proof Construction by Tactics
Gilles Dowek
In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them…
A Unification Algorithm for Second-Order Linear Terms
Gilles Dowek
We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence.