COMPARISON OF NATURAL DEDUCTION AND LOCKING RESOLUTION IMPLEMENTATIONSGREENBAUM S; NAGASAKA A; O'RORKE P et al.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 159-171; BIBL. 16 REF.Conference Paper

A LANGUAGE FOR EXPRESSING MATHEMATICAL KNOWLEDGE IN AUTOMATIC THEOREM PROVINGPASTRE D.1982; ECAI 82. EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE/1982-07-12/ORSAY; DEU; KAISERLAUTERN: IMPR. ABTEILUNG FOTO-REPRO-DRUCK DER UNIVERSITAET KAISERLAUTERN; DA. 1982; PP. 116-118; BIBL. 29 REF.Conference Paper

A natural extension of natural deductionSCHROEDER-HEISTER, P.The Journal of symbolic logic. 1984, Vol 49, Num 4, pp 1284-1300, issn 0022-4812Article

Gentzenization and Decidability of Some Contraction-Less Relevant LogicsBRADY, R. T.Journal of philosophical logic. 1991, Vol 20, Num 1, pp 97-117, issn 0022-3611Article

Linear logic, coherence and dinaturalityBLUTE, R.Theoretical computer science. 1993, Vol 115, Num 1, pp 3-41, issn 0304-3975Conference Paper

Translation of resolution proofs into short first-order proofs without choice axiomsDE NIVELLE, Hans.Information and computation (Print). 2005, Vol 199, Num 1-2, pp 24-54, issn 0890-5401, 31 p.Conference Paper

A logic for category theoryGILMORE, P. C; TSIKNIS, G. K.Theoretical computer science. 1993, Vol 111, Num 1-2, pp 211-252, issn 0304-3975Conference Paper

Automation for interactive proof : First prototypeJIA MENG; QUIGLEY, Claire; PAULSON, Lawrence C et al.Information and computation (Print). 2006, Vol 204, Num 10, pp 1575-1596, issn 0890-5401, 22 p.Article

Relevant implication and the case for a weaker logicBRADY, R. T.Journal of philosophical logic. 1996, Vol 25, Num 2, pp 151-183, issn 0022-3611Article

Logical foundations for programming semanticsGILMORE, P. C; TSIKNIS, G. K.Theoretical computer science. 1993, Vol 111, Num 1-2, pp 253-290, issn 0304-3975Conference Paper

On the expressive power of schemesDOWEK, Gilles; YING JIANG.Information and computation (Print). 2011, Vol 209, Num 9, pp 1231-1245, issn 0890-5401, 15 p.Article

A modal logic internalizing normal proofsPARK, Sungwoo; IM, Hyeonseung.Information and computation (Print). 2011, Vol 209, Num 12, pp 1519-1535, issn 0890-5401, 17 p.Article

L'Arithmétique fonctionnelle du second ordre avec points fixes = Second order functional arithmetic with fixpointsRaffalli, Christophe; Krivine, J.-L.1994, 116 p.Thesis

κ-Valued non-associative Lambek grammars are learnable from generalized functor-argument structuresBECHET, Denis; FORET, Annie.Theoretical computer science. 2006, Vol 355, Num 2, pp 139-152, issn 0304-3975, 14 p.Article

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level termsGABBAY, Murdoch J; MULLIGAN, Dominic P.Information and computation (Print). 2010, Vol 208, Num 3, pp 230-258, issn 0890-5401, 29 p.Article

Pedagogical second-order λ-calculusCOLSON, Loic; MICHEL, David.Theoretical computer science. 2009, Vol 410, Num 42, pp 4190-4203, issn 0304-3975, 14 p.Article