34 citations · 144 across the 66 of their papers we have counts for
5 papers · 2 filters
SCTL: Towards Combining Model Checking and Proof Checking
Ying Jiang, Jian Liu, Gilles Dowek +1
Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at comb…
On the definition of the classical connectives and quantifiers
Gilles Dowek
Classical logic is embedded into constructive logic, through a definition of the classical connectives and quantifiers in terms of the constructive ones.
Decidability, Introduction Rules and Automata
Gilles Dowek, Ying Jiang
We present a method to prove the decidability of provability in several well-known inference systems. This method generalizes both cut-elimination and the construction of an automa…
Rules and derivations in an elementary logic course
Gilles Dowek
When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of…
Two linearities for quantum computing in the lambda calculus
Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while t…