, le_S : (n,m:nat)(le n m) -> (le n (S m))
, Axiom monoticity : (n,m:nat)(le n m) -> (le (f n) (f m))
, Lemma le_x_Sx : (x:nat)(le x (S x))
, Theorem L1 : (a:nat)
, At last, let us show some examples on which the tactic fails
, Error: Not provable in DPC, vol.2
,
A decision procedure revisited : Notes on direct logic, linear logic and its implementation, Theoretical Computer Science, vol.95, pp.115-142, 1992. ,
The Coq Proof Assistant Reference Manual Version 5, INRIA, vol.10, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00069994
Constructive Logics. Part I: A Tutorial on Proof Systems and Typed {Calculi, Digital Equipment Corporation, vol.8, 1991. ,
Constructive Logics. Part II: Linear Logic and Proof Nets, Digital Equipment Corporation, vol.8, 1991. ,
Proofs and Types. C a m bridge Tracts in Theoretical Computer Science 7, 1989. ,
A decidable fragment of Predicate Calculus, Theoretical Computer Science, vol.32, pp.297-307, 1984. ,
Etudes et recherches en Informatique, 1990. ,
Manuel de r ef erence du langage Caml. I n terEditions, 1993. ,
Proof search in rst-order linear logic and other cut-free sequent calculi, Symposium on Logic in Computer Science, 1994. ,
An eecient uniication algorithm, ACM Trans. Prog. Lang. Syst, vol.4, issue.2, pp.258-282, 1982. ,
Le langage Caml. I n terEditions, 1993. ,