Proof-search in type-theoretic languages: An introduction. (English) Zbl 0952.03006
Summary: We introduce the main concepts and problems in the theory of proof-search in type-theoretic languages and survey some specific, connected topics. We do not claim to cover all of the theoretical and implementation issues in the study of proof-search in type-theoretic languages; rather, we present some key ideas and problems, starting from well-motivated points of departure such as a definition of a type-theoretic language or the relationship between languages and proof-objects. The strong connections between different proof-search methods in logics, type theories and logical frameworks, together with their impact on programming and implementation issues, are central in this context.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B15 | Higher-order logic; type theory (MSC2010) |
| 03F03 | Proof theory in general (including proof-theoretic semantics) |
| 68N18 | Functional programming and lambda calculus |
| 03B70 | Logic in computer science |
Software:
LEGO; Nuprl; PVS; TPS; HOL; Lolli; Elf; SKIL; Jape; XBarnacle; Cambridge LCF; Automath; IsabelleReferences:
| [1] | Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, J. Symbolic Logic, 59, 2, 543-574 (1994) · Zbl 0822.03007 |
| [2] | Abrusci, V. M., Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, J. Symbolic Logic, 56, 4, 1403-1451 (1991) · Zbl 0746.03044 |
| [3] | P. Anderson, Representing proof transformations for program optimization, in: 12th Internat. Conf. on Automated Deduction, CADE-12, LNAI 814, Nancy, France, July 1994, pp. 575-589.; P. Anderson, Representing proof transformations for program optimization, in: 12th Internat. Conf. on Automated Deduction, CADE-12, LNAI 814, Nancy, France, July 1994, pp. 575-589. · Zbl 1433.68091 |
| [4] | Andreoli, J. M., Logic programming with focusing proofs in linear logic, J. Logic Comput., 2, 3, 297-347 (1992) · Zbl 0764.03020 |
| [5] | Andreoli, J. M.; Pareschi, R., Linear objects: logical processes with built-in inheritance, New Generation Comput., 9, 445-473 (1991) · Zbl 0731.68022 |
| [6] | Andrews, P., Theorem proving via general mating, J. ACM, 28, 2, 193-214 (1981) · Zbl 0456.68119 |
| [7] | Andrews, P. B., On connections and higher-order logic, J. Automat. Reason., 5, 257-291 (1989) · Zbl 0694.03011 |
| [8] | Andrews, P. B.; Bishop, M.; Issar, S.; Nesmith, D.; Pfenning, F.; Xi, H., TPS: a theorem proving system for classical type theory, J. Automat. Reason., 16, 321-353 (1996) · Zbl 0858.03017 |
| [9] | Avron, A., Simple consequence relations, Inform. Comput., 92, 105-139 (1991) · Zbl 0733.03007 |
| [10] | Avron, A., Some properties of linear logic proved by semantics methods, J. Logic Comput., 4, 6, 929-938 (1994) · Zbl 0814.03006 |
| [11] | Avron, A.; Honsell, F.; Mason, I. A.; Pollack, R., Using typed lambda calculus to implement formal systems on a machine, J. Automat. Reason., 9, 309-354 (1992) · Zbl 0784.68072 |
| [12] | A. Avron, F. Honsell, M. Miculan, C. Paravano, Encoding modal logics in logical frameworks, Stud. Logica 60(1) (1998).; A. Avron, F. Honsell, M. Miculan, C. Paravano, Encoding modal logics in logical frameworks, Stud. Logica 60(1) (1998). · Zbl 0954.03021 |
| [13] | V. Balat, D. Galmiche, Proof systems for Intuitionistic Provability in Linear Logic, in: Internat. Workshop on Labelled Deduction LD’98, Freiburg, Germany, September 1998.; V. Balat, D. Galmiche, Proof systems for Intuitionistic Provability in Linear Logic, in: Internat. Workshop on Labelled Deduction LD’98, Freiburg, Germany, September 1998. · Zbl 0968.03064 |
| [14] | H.P. Barendregt, Lambda calculi with types, in: S. Abramsky, D.M. Gabbay, T.S.E. Maibaum (Eds.), Background: Computational Structures, Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford, England, 1992, pp. 117-309.; H.P. Barendregt, Lambda calculi with types, in: S. Abramsky, D.M. Gabbay, T.S.E. Maibaum (Eds.), Background: Computational Structures, Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford, England, 1992, pp. 117-309. · Zbl 0777.68001 |
| [15] | H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103, revised Edition, North-Holland, Amsterdam, 1984.; H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103, revised Edition, North-Holland, Amsterdam, 1984. · Zbl 0551.03007 |
| [16] | N. Benton, G. Bierman, V. de Paiva, M. Hyland, Linear \(λ\)-calculus and categorical models revisited, in: 6th Workshop CSL’92, San Miniato, Italy, Lecture Notes in Computer Science, vol. 702, Springer, Berlin, 1992, pp. 61-84.; N. Benton, G. Bierman, V. de Paiva, M. Hyland, Linear \(λ\)-calculus and categorical models revisited, in: 6th Workshop CSL’92, San Miniato, Italy, Lecture Notes in Computer Science, vol. 702, Springer, Berlin, 1992, pp. 61-84. · Zbl 0840.03003 |
| [17] | Bibel, W., On matrices with connections, J. ACM, 28, 4, 633-645 (1981) · Zbl 0468.68097 |
| [18] | G.M. Bierman, Towards a classical linear \(λ\)-calculus (preliminary report), Electronic Notes in Theoretical Computer Science, vol. 3, 1996.; G.M. Bierman, Towards a classical linear \(λ\)-calculus (preliminary report), Electronic Notes in Theoretical Computer Science, vol. 3, 1996. · Zbl 0908.03020 |
| [19] | O. Bittel, Tableau-based theorem proving and synthesis of \(λ\)-terms in the intuitionistic logic, in: European Workshop JELIA ’92, Lecture Notes in Artificial Intelligence, vol. 633, 1992, pp. 262-278.; O. Bittel, Tableau-based theorem proving and synthesis of \(λ\)-terms in the intuitionistic logic, in: European Workshop JELIA ’92, Lecture Notes in Artificial Intelligence, vol. 633, 1992, pp. 262-278. · Zbl 0925.03083 |
| [20] | R. Bornat, B. Sufrin, Animating formal proof at the surface: the Jape proof calculator, Comput. J., to appear.; R. Bornat, B. Sufrin, Animating formal proof at the surface: the Jape proof calculator, Comput. J., to appear. |
| [21] | E. Boudinet, D. Galmiche, Proofs, concurrent objects and computations in a FILL framework, in Workshop on Object-based Parallel and Distributed Computation, OBPDC’95, Lecture Notes in Computer Science, vol. 1107, Springer, Berlin, Tokyo, Japan, 1996, pp. 148-167.; E. Boudinet, D. Galmiche, Proofs, concurrent objects and computations in a FILL framework, in Workshop on Object-based Parallel and Distributed Computation, OBPDC’95, Lecture Notes in Computer Science, vol. 1107, Springer, Berlin, Tokyo, Japan, 1996, pp. 148-167. |
| [22] | J. Brown, L. Wallen, Representing unification in a logical framework, September 1995.; J. Brown, L. Wallen, Representing unification in a logical framework, September 1995. |
| [23] | A. Bundy, The Computer Modelling of Mathematical Reasoning, Academic Press, New York, 1983.; A. Bundy, The Computer Modelling of Mathematical Reasoning, Academic Press, New York, 1983. · Zbl 0541.68067 |
| [24] | A. Bundy, The use of explicit plans to guide proofs, in: E. Lusk, R. Overbeek (Eds.), Lecture Notes in Computer Science, vol. 310, Proc. CADE-9, Springer, Berlin, 1988, pp. 111-120.; A. Bundy, The use of explicit plans to guide proofs, in: E. Lusk, R. Overbeek (Eds.), Lecture Notes in Computer Science, vol. 310, Proc. CADE-9, Springer, Berlin, 1988, pp. 111-120. · Zbl 0656.68106 |
| [25] | A. Bundy, A science of reasoning, in: J.-L. Lassez, G.D. Plotkin (Eds.), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA, 1991, pp. 178-198.; A. Bundy, A science of reasoning, in: J.-L. Lassez, G.D. Plotkin (Eds.), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA, 1991, pp. 178-198. · Zbl 0793.03002 |
| [26] | A. Bundy, F. van Harmelen, C. Horn, A. Smaill, The use of explicit plans to guide proofs, in: M. Stickel (Ed.), Lecture Notes in Computer Science, vol. 449, Proc. CADE-10, Springer, Berlin, 1990, pp. 647-648.; A. Bundy, F. van Harmelen, C. Horn, A. Smaill, The use of explicit plans to guide proofs, in: M. Stickel (Ed.), Lecture Notes in Computer Science, vol. 449, Proc. CADE-10, Springer, Berlin, 1990, pp. 647-648. · Zbl 1509.68299 |
| [27] | F. Cantu, A. Bundy, A. Smaill, D. Basin, Experiments in automating hardware verification using inductive proof planning, in: M. Srivas, A Camilleri (Eds.), Lecture Notes in Computer Science, vol. 1166, Springer, Berlin, 1996, pp. 94-108.; F. Cantu, A. Bundy, A. Smaill, D. Basin, Experiments in automating hardware verification using inductive proof planning, in: M. Srivas, A Camilleri (Eds.), Lecture Notes in Computer Science, vol. 1166, Springer, Berlin, 1996, pp. 94-108. |
| [28] | Cartmell, J., Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic, 32, 209-243 (1994) · Zbl 0634.18003 |
| [29] | I. Cervesato, A linear logical framework, Ph.D. Thesis, Università di Torino, 1996 (in Italian).; I. Cervesato, A linear logical framework, Ph.D. Thesis, Università di Torino, 1996 (in Italian). · Zbl 1031.03056 |
| [30] | I. Cervesato, F. Pfenning, Linear higher-order pre-unification, in: CADE Workshop on Proof-Search in Type-Theoretic Languages, Rutgers University, New Brunswick, USA, 1996, pp. 41-48.; I. Cervesato, F. Pfenning, Linear higher-order pre-unification, in: CADE Workshop on Proof-Search in Type-Theoretic Languages, Rutgers University, New Brunswick, USA, 1996, pp. 41-48. |
| [31] | I. Cervesato, F. Pfenning, A linear logical framework, in 11th IEEE Symp. on Logic in Computer Science, New Brunswick, New Jersey, July 1996, pp. 264-275.; I. Cervesato, F. Pfenning, A linear logical framework, in 11th IEEE Symp. on Logic in Computer Science, New Brunswick, New Jersey, July 1996, pp. 264-275. · Zbl 1031.03056 |
| [32] | B. Chellas, Modal Logic, Cambridge University Press, Cambridge, 1980.; B. Chellas, Modal Logic, Cambridge University Press, Cambridge, 1980. · Zbl 0431.03009 |
| [33] | J. Chirimar, Proof theoretic approach to specification languages, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania, 1995.; J. Chirimar, Proof theoretic approach to specification languages, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania, 1995. |
| [34] | T. Coquand, On the Analogy Between Propositions and Types, The UT Year of Programming Series: Logical Foundations of Functional Programming, Addison-Wesley, Reading, MA, 1990, pp. 399-417.; T. Coquand, On the Analogy Between Propositions and Types, The UT Year of Programming Series: Logical Foundations of Functional Programming, Addison-Wesley, Reading, MA, 1990, pp. 399-417. · Zbl 0709.68003 |
| [35] | Coquand, T.; Huet, G., The calculus of constructions, Inform. and Comput., 76, 95-120 (1988) · Zbl 0654.03045 |
| [36] | Coquand, T.; Nordström, B.; Smith, J.; Van Sydo, B., Type Theory and Programming, Bulletin of the EATCS, 52, 203-228 (1994) · Zbl 0791.68017 |
| [37] | M. D’Agostino, D.M. Gabbay, A generalization of analytic deduction via labelled deductive systems. Part I: basic substructural logics, J. Automat. Reason. 13 (1994) 243-281.; M. D’Agostino, D.M. Gabbay, A generalization of analytic deduction via labelled deductive systems. Part I: basic substructural logics, J. Automat. Reason. 13 (1994) 243-281. · Zbl 0816.03012 |
| [38] | B.J. Day, On closed categories of functors, in: S. Mac Lane (Ed.), Reports of the Midwest Category Seminar, Lecture Notes in Mathematics, vol. 137, Springer, Berlin, 1970, pp. 1-38.; B.J. Day, On closed categories of functors, in: S. Mac Lane (Ed.), Reports of the Midwest Category Seminar, Lecture Notes in Mathematics, vol. 137, Springer, Berlin, 1970, pp. 1-38. · Zbl 0203.31402 |
| [39] | G. Delzanno, D. Galmiche, M. Martelli, A specification logic for concurrent object-oriented programming, Math. Struct. Comput. Sci. (1999) to appear.; G. Delzanno, D. Galmiche, M. Martelli, A specification logic for concurrent object-oriented programming, Math. Struct. Comput. Sci. (1999) to appear. · Zbl 0931.68066 |
| [40] | Dowek, G., A complete proof synthesis method for the cube of type systems, J. Logic Comput., 3, 3, 287-315 (1993) · Zbl 0789.68123 |
| [41] | M. Dummett, Elements of Intuitionism, Oxford University Press, Oxford, 1977.; M. Dummett, Elements of Intuitionism, Oxford University Press, Oxford, 1977. · Zbl 0358.02032 |
| [42] | Dyckhoff, R., Contraction-free sequent calculi for intuitionistic logic, J. Symbolic Logic, 57, 795-807 (1992) · Zbl 0761.03004 |
| [43] | U. Egly, S. Schmitt, Intuitionistic proof transformations and their application to constructive program synthesis, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Lindau, Germany, 1998, pp. 19-30.; U. Egly, S. Schmitt, Intuitionistic proof transformations and their application to constructive program synthesis, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Lindau, Germany, 1998, pp. 19-30. · Zbl 0924.03042 |
| [44] | C.M. Elliot, Higher-order unification with dependent function types, in 3rd Internat. Conf. RTA 89, Chapell Hill, North Carolina, Lecture Notes in Computer Science, vol. 355, Springer, Berlin, April 1989, pp. 121-136.; C.M. Elliot, Higher-order unification with dependent function types, in 3rd Internat. Conf. RTA 89, Chapell Hill, North Carolina, Lecture Notes in Computer Science, vol. 355, Springer, Berlin, April 1989, pp. 121-136. · Zbl 1503.68289 |
| [45] | C. Elliott, Extensions and applications of higher-order unification, Ph.D. Thesis, Carnegie Mellon University, 1990.; C. Elliott, Extensions and applications of higher-order unification, Ph.D. Thesis, Carnegie Mellon University, 1990. |
| [46] | Engberg, U.; Winskel, G., Completeness results for linear logic on petri nets, Ann. Pure Appl. Logic, 86, 101-135 (1997) · Zbl 0873.03005 |
| [47] | R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, NJ, 1986.; R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, NJ, 1986. |
| [48] | A. Felty, D. Miller, Encoding a dependent-type \(λ\)-calculus in a logic programming language, in 10th Internat. Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 449, Kaiserslautern, FRG, July 1990, pp. 221-235.; A. Felty, D. Miller, Encoding a dependent-type \(λ\)-calculus in a logic programming language, in 10th Internat. Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 449, Kaiserslautern, FRG, July 1990, pp. 221-235. · Zbl 0708.68090 |
| [49] | J. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Wiley, New York, 1986.; J. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Wiley, New York, 1986. · Zbl 0605.03004 |
| [50] | Galmiche, D., Program development in constructive type theory, Theoret. Comput. Sci., 94, 2, 237-259 (1992) · Zbl 0760.68012 |
| [51] | D. Galmiche, O. Hermann, SKIL: a system for programming with proofs, in LPAR’93, Internat. Conf. Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 698, St. Petersburg, Russia, July 1993, pp. 348-350.; D. Galmiche, O. Hermann, SKIL: a system for programming with proofs, in LPAR’93, Internat. Conf. Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 698, St. Petersburg, Russia, July 1993, pp. 348-350. · Zbl 0797.68143 |
| [52] | D. Galmiche, D. Larchey-Wendling, Provability in intuitionistic linear logic from a new interpretation on Petri nets — extended abstract, Electronic Notes in Theoret. Comput. Sci. 17 (1998).; D. Galmiche, D. Larchey-Wendling, Provability in intuitionistic linear logic from a new interpretation on Petri nets — extended abstract, Electronic Notes in Theoret. Comput. Sci. 17 (1998). · Zbl 0917.68158 |
| [53] | D. Galmiche, B. Martin, Proof search and proof nets construction in linear logic, in 4th Workshop on Logic, Language, Information and Computation, Wollic’97, Fortaleza, Brasil, August 1997. Logic J. IGPL 5-6 (1997) 883-885.; D. Galmiche, B. Martin, Proof search and proof nets construction in linear logic, in 4th Workshop on Logic, Language, Information and Computation, Wollic’97, Fortaleza, Brasil, August 1997. Logic J. IGPL 5-6 (1997) 883-885. · Zbl 0917.68199 |
| [54] | D. Galmiche, B. Martin, Proof nets construction and automated deduction in non-commutative linear logic — extended abstract, Electronic Notes in Theoret. Comput. Sci. 17 (1998).; D. Galmiche, B. Martin, Proof nets construction and automated deduction in non-commutative linear logic — extended abstract, Electronic Notes in Theoret. Comput. Sci. 17 (1998). · Zbl 0917.68199 |
| [55] | D. Galmiche, G. Perrier, A procedure for automatic proof nets construction, in LPAR’92, Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 42-53.; D. Galmiche, G. Perrier, A procedure for automatic proof nets construction, in LPAR’92, Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 42-53. · Zbl 0920.03015 |
| [56] | D. Galmiche, G. Perrier, Foundations of proof search strategies design in linear logic, in Logic at St Petersburg ’94, Symp. on Logical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 813, Springer, Berlin, St. Petersburg, Russia, July 1994, pp. 101-113.; D. Galmiche, G. Perrier, Foundations of proof search strategies design in linear logic, in Logic at St Petersburg ’94, Symp. on Logical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 813, Springer, Berlin, St. Petersburg, Russia, July 1994, pp. 101-113. · Zbl 0964.03512 |
| [57] | Galmiche, D.; Perrier, G., On proof normalization in linear logic, Theoret. Comput. Sci., 135, 1, 67-110 (1994) · Zbl 0815.03033 |
| [58] | G. Gentzen, Untersuchungen über das logische Schliessen, Math. Z. 39 (1934) 176-210, 405-431.; G. Gentzen, Untersuchungen über das logische Schliessen, Math. Z. 39 (1934) 176-210, 405-431. · Zbl 0010.14501 |
| [59] | D. Gillies, Artificial Intelligence and Scientific Method, Oxford University Press, Oxford, 1997.; D. Gillies, Artificial Intelligence and Scientific Method, Oxford University Press, Oxford, 1997. · Zbl 0917.68174 |
| [60] | Girard, J. Y., The system F of variables types, fifteen years later, Theoret. Comput. Sci., 45, 159-192 (1986) · Zbl 0623.03013 |
| [61] | Girard, J. Y., Linear logic, Theoret. Comput. Sci., 50, (1987) (1) · Zbl 0625.03037 |
| [62] | J.Y. Girard, Linear logic: its syntax and semantics, in: J.Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge University Press, Cambridge, 1995, pp. 1-42.; J.Y. Girard, Linear logic: its syntax and semantics, in: J.Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge University Press, Cambridge, 1995, pp. 1-42. · Zbl 0828.03003 |
| [63] | J.Y. Girard, Proof nets: the parallel syntax for proof theory, in: Ursini, Agliano (Eds.), Logic and Algebra, M. Dekker, New York, 1995.; J.Y. Girard, Proof nets: the parallel syntax for proof theory, in: Ursini, Agliano (Eds.), Logic and Algebra, M. Dekker, New York, 1995. · Zbl 0868.03025 |
| [64] | J.Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1989.; J.Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1989. |
| [65] | M.J. Gordon, R. Milner, C.P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science, vol. 78, Springer, Berlin, 1979.; M.J. Gordon, R. Milner, C.P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science, vol. 78, Springer, Berlin, 1979. · Zbl 0421.68039 |
| [66] | M.J.C Gordon, Hol: a proof generating system for higher-order logic, in: G. Birtwistle, P.A. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, 1988, pp. 73-128.; M.J.C Gordon, Hol: a proof generating system for higher-order logic, in: G. Birtwistle, P.A. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, 1988, pp. 73-128. |
| [67] | Harland, J., A proof-theoretic analysis of goal-directed provability, J. Logic Comput., 4, 1, 69-88 (1994) · Zbl 0793.03060 |
| [68] | J. Harland, D. Pym, Resource-distribution via boolean constraints (extended abstract), in 14th Internat. Conf. on Automated Deduction, CADE-12, Lecture Notes in Artificial Intelligence, vol. 814, Townsville, North Queensland, Australia, July 1997, pp. 222-236.; J. Harland, D. Pym, Resource-distribution via boolean constraints (extended abstract), in 14th Internat. Conf. on Automated Deduction, CADE-12, Lecture Notes in Artificial Intelligence, vol. 814, Townsville, North Queensland, Australia, July 1997, pp. 222-236. · Zbl 1422.03129 |
| [69] | J.A. Harland, D.J. Pym, M. Winikoff, Programming in Lygon: an overview, in: M. Wirsing, M. Nivat (Eds.), Proc. AMAST ’96, Lecture Notes in Computer Science, vol. 1101, Springer, Berlin, 1996, pp. 391-405.; J.A. Harland, D.J. Pym, M. Winikoff, Programming in Lygon: an overview, in: M. Wirsing, M. Nivat (Eds.), Proc. AMAST ’96, Lecture Notes in Computer Science, vol. 1101, Springer, Berlin, 1996, pp. 391-405. |
| [70] | Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J. ACM, 40, 143-184 (1993) · Zbl 0778.03004 |
| [71] | Harper, R.; Sannella, D.; Tarlecki, A., Structured theory presentations and logic representations, Ann. Pure Appl. Logic, 67, 113 (1994) · Zbl 0809.03019 |
| [72] | Harper, R. W.; Honsell, F.; Plotkin, G. D., A framework for defining logics, J. ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004 |
| [73] | L. Helmink, Resolution and type theory, in ESOP 90, Lecture Notes in Computer Science, vol. 432, Springer, Berlin, Copenhagen, Denmark, May 1990, pp. 197-211.; L. Helmink, Resolution and type theory, in ESOP 90, Lecture Notes in Computer Science, vol. 432, Springer, Berlin, Copenhagen, Denmark, May 1990, pp. 197-211. · Zbl 0765.68175 |
| [74] | Hodas, J.; Miller, D., Logic programming in a fragment of intuitionistic linear logic, J. Inform. Comput., 110, 327-365 (1994) · Zbl 0807.68016 |
| [75] | J. Hodas, J. Polakow, Forum as a logic programming language (Preliminary Report), Electronic Notes in Theoret. Comput. Sci. 3 (1996).; J. Hodas, J. Polakow, Forum as a logic programming language (Preliminary Report), Electronic Notes in Theoret. Comput. Sci. 3 (1996). · Zbl 0909.68035 |
| [76] | Hodas, J. S.; Miller, D., Logic programming in a fragment of intuitionistic linear logic, Inform. and Comput., 110, 2, 327-365 (1994) · Zbl 0807.68016 |
| [77] | C.J. Hogger, Essentials of Logic Programming, Clarendon Press, Oxford, 1990.; C.J. Hogger, Essentials of Logic Programming, Clarendon Press, Oxford, 1990. · Zbl 0705.68030 |
| [78] | W.A. Howard, The formulae-as-types notion of construction, in: To H.B. Curry: Essays in Combinatory Logic, \(λ\)-Calculus and Formalism, Academic Press, New York, 1980, pp. 479-490.; W.A. Howard, The formulae-as-types notion of construction, in: To H.B. Curry: Essays in Combinatory Logic, \(λ\)-Calculus and Formalism, Academic Press, New York, 1980, pp. 479-490. |
| [79] | D.J. Howe, Sematic foundations for embedding HOL in Nuprl, in 5th Internat. Conf. on Algebraic Methods and Software Technology, AMAST’96, Lecture Notes in Computer Science, vol. 1101, Springer, Berlin, Munich, Germany, July 1996, pp. 85-101.; D.J. Howe, Sematic foundations for embedding HOL in Nuprl, in 5th Internat. Conf. on Algebraic Methods and Software Technology, AMAST’96, Lecture Notes in Computer Science, vol. 1101, Springer, Berlin, Munich, Germany, July 1996, pp. 85-101. · Zbl 0886.03008 |
| [80] | G. Huet, Résolution d’équations dans les languages d’ordre 1, 2, …, \(ω\), Thèse de Doctorat d’État, Université de Paris VII, 1976.; G. Huet, Résolution d’équations dans les languages d’ordre 1, 2, …, \(ω\), Thèse de Doctorat d’État, Université de Paris VII, 1976. |
| [81] | Huet, G., A unification algorithm for typed \(λ\)-calculus, Theoret. Comput. Sci., 1, 27-57 (1975) · Zbl 0337.68027 |
| [82] | G. Huet, A Uniform Approach to Type Theory, The UT Year of Programming Series, Addison-Wesley, Reading, MA, 1990, pp. 337-398 (Chapter 16).; G. Huet, A Uniform Approach to Type Theory, The UT Year of Programming Series, Addison-Wesley, Reading, MA, 1990, pp. 337-398 (Chapter 16). |
| [83] | A. Ireland, The use of planning critics in mechanizing inductive proofs, in: A. Voronkov (Ed.), Lecture Notes in Computer Science, vol. 624, Proc. LPAR 92, Springer, Berlin, 1992, pp. 178-189.; A. Ireland, The use of planning critics in mechanizing inductive proofs, in: A. Voronkov (Ed.), Lecture Notes in Computer Science, vol. 624, Proc. LPAR 92, Springer, Berlin, 1992, pp. 178-189. |
| [84] | Ireland, A.; Bundy, A., Productive use of failure in inductive proof, J. Automat. Reason., 16, 1-2, 79-111 (1996) · Zbl 0847.68103 |
| [85] | S.S. Ishtiaq, D.J. Pym, Kripke resource models of a dependently-typed, bunched \(λ\)-calculus, in preparation.; S.S. Ishtiaq, D.J. Pym, Kripke resource models of a dependently-typed, bunched \(λ\)-calculus, in preparation. · Zbl 1017.03005 |
| [86] | Ishtiaq, S. S.; Pym, D. J., A relevant analysis of natural deduction, J. Logic Comput., 8, 6, 809-838 (1998) · Zbl 0915.03022 |
| [87] | B. Jacobs, Categorical type theory, Ph.D. Thesis, Catholic University, Nijmegen, September 1991.; B. Jacobs, Categorical type theory, Ph.D. Thesis, Catholic University, Nijmegen, September 1991. |
| [88] | N. Kobayashi, A. Yonezawa, ACL — a concurrent linear logic programming paradigm, in Internat. Symp. on Logic Programming, Vancouver, October 1993, pp. 279-294.; N. Kobayashi, A. Yonezawa, ACL — a concurrent linear logic programming paradigm, in Internat. Symp. on Logic Programming, Vancouver, October 1993, pp. 279-294. |
| [89] | Kobayashi, N.; Yonezawa, A., Asynchronous communication model based on linear logic, Formal Aspects Comput., 3, 279-294 (1994) |
| [90] | N. Kobayashi, A. Yonezawa, Type-theoretic foundations for concurrent object-oriented programming, in: ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages and Applications, OOPSLA’94, 1994, pp. 31-45.; N. Kobayashi, A. Yonezawa, Type-theoretic foundations for concurrent object-oriented programming, in: ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages and Applications, OOPSLA’94, 1994, pp. 31-45. |
| [91] | R. Kowalski, Logic for Problem Solving, Elsevier, Amsterdam, 1979.; R. Kowalski, Logic for Problem Solving, Elsevier, Amsterdam, 1979. · Zbl 0426.68002 |
| [92] | C. Kreitz, H. Mantel, J. Otten, S. Schmitt, Connection-based proof construction in linear logic, in: 14th Internat. Conf. on Automated Deduction, Townsville, North Queensland, Australia, 1997, pp. 207-221.; C. Kreitz, H. Mantel, J. Otten, S. Schmitt, Connection-based proof construction in linear logic, in: 14th Internat. Conf. on Automated Deduction, Townsville, North Queensland, Australia, 1997, pp. 207-221. · Zbl 1430.03040 |
| [93] | J. Lambek, P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, 1987.; J. Lambek, P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, 1987. · Zbl 0596.03002 |
| [94] | P. Lincoln, N. Shankar, Proof search in first-order linear logic and other cut-free sequent calculi, in: 9th IEEE Symp. on Logic in Computer Science, Paris, France, July 1994, pp. 282-291.; P. Lincoln, N. Shankar, Proof search in first-order linear logic and other cut-free sequent calculi, in: 9th IEEE Symp. on Logic in Computer Science, Paris, France, July 1994, pp. 282-291. |
| [95] | P.D. Lincoln, J.C. Mitchell, A. Scedrov, Stochastic interaction and linear logic, in: J.Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge University Press, Cambridge, 1995, pp. 147-166.; P.D. Lincoln, J.C. Mitchell, A. Scedrov, Stochastic interaction and linear logic, in: J.Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge University Press, Cambridge, 1995, pp. 147-166. · Zbl 0829.03032 |
| [96] | P.D. Lincoln, J.C. Mitchell, A. Scedrov, Linear logic proof games and optimization, Bull. Symbolic Logic 2(3) (1996).; P.D. Lincoln, J.C. Mitchell, A. Scedrov, Linear logic proof games and optimization, Bull. Symbolic Logic 2(3) (1996). · Zbl 0862.03023 |
| [97] | H. Lowe, D. Duncan, Xbarnacle: making theorem provers more accessible, in: W. McCune (Ed.), 14th Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 1249, Springer, Berlin, 1997, pp. 404-408.; H. Lowe, D. Duncan, Xbarnacle: making theorem provers more accessible, in: W. McCune (Ed.), 14th Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 1249, Springer, Berlin, 1997, pp. 404-408. |
| [98] | Z. Luo, R. Pollack, LEGO proof development system: user’s manual, LFCS Technical Report ECS-LFCS-92-211, Edinburgh, 1992.; Z. Luo, R. Pollack, LEGO proof development system: user’s manual, LFCS Technical Report ECS-LFCS-92-211, Edinburgh, 1992. |
| [99] | P. Madden, Automatic program optimization through proof transformation, in: 11th Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, June 1992, pp. 446-460.; P. Madden, Automatic program optimization through proof transformation, in: 11th Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, June 1992, pp. 446-460. |
| [100] | L. Magnussen, B. Nordström, The ALF proof editor and its proof engine, in Workshop on Types for Proofs and Programs, Nijmegen, The Netherlands, 1993.; L. Magnussen, B. Nordström, The ALF proof editor and its proof engine, in Workshop on Types for Proofs and Programs, Nijmegen, The Netherlands, 1993. |
| [101] | P. Manoury, M. Parigot, M. Simonot, Propre: a programming language with proofs, in Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 484-486.; P. Manoury, M. Parigot, M. Simonot, Propre: a programming language with proofs, in Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 484-486. |
| [102] | P. Martin-Löf, An intuitionnistic theory of types, in Logic Colloquium ’73, North-Holland, Amsterdam, 1973, pp. 73-118.; P. Martin-Löf, An intuitionnistic theory of types, in Logic Colloquium ’73, North-Holland, Amsterdam, 1973, pp. 73-118. · Zbl 0334.02016 |
| [103] | P. Martin-Löf, Constructive mathematics and computer programming, in 6th Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982, pp. 153-175.; P. Martin-Löf, Constructive mathematics and computer programming, in 6th Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982, pp. 153-175. · Zbl 0541.03034 |
| [104] | P. Martin-Löf, Intuitionistic Type Theory, Studies in Proof Theory, Lectures Notes, Bibliopolis, 1984.; P. Martin-Löf, Intuitionistic Type Theory, Studies in Proof Theory, Lectures Notes, Bibliopolis, 1984. |
| [105] | Masseron, M.; Tollu, C.; Vauzeilles, J., Generating plans in linear logic I: actions as proofs, Theoret. Comput. Sci., 113, (1993) (2) · Zbl 0787.03006 |
| [106] | Meseguer, J.; Marti-Oliet, N., From Petri nets to linear logic, Math. Struct. Comput. Sci., 1, 69-101 (1991) · Zbl 0746.03057 |
| [107] | Miller, D., A logical analysis of modules in logic programming, J. Logic Programm., 6, 2, 79-108 (1989) · Zbl 0681.68022 |
| [108] | Miller, D., Forum: a multiple-conclusion specification logic, Theoret. Comput. Sci., 165, 1, 201-232 (1996) · Zbl 0872.68019 |
| [109] | Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Logic, 51, 125-157 (1991) · Zbl 0721.03037 |
| [110] | G. Mints, Gentzen type systems and resolution rules, in: P. Martin-Löf, G. Mints (Eds.), COLOG 88, Lecture Notes in Computer Science, vol. 417, Springer, Berlin, Tallinn, Estonia, 1988, pp. 198-231.; G. Mints, Gentzen type systems and resolution rules, in: P. Martin-Löf, G. Mints (Eds.), COLOG 88, Lecture Notes in Computer Science, vol. 417, Springer, Berlin, Tallinn, Estonia, 1988, pp. 198-231. · Zbl 0739.03011 |
| [111] | Mints, G., Resolution calculus for the first order linear logic, J. Logic Language Inform., 2, 59-83 (1993) · Zbl 0793.03006 |
| [112] | Mitchell, J.; Moggi, E., Kripke-style models for typed lambda calculus, Ann. Pure Appl. Logic, 51, 99-124 (1981) · Zbl 0728.03011 |
| [113] | G. Nadathur, D. Miller, Higher-order logic programming, Handbook of Logic in AI and Logic Progamming, vol. 5, Oxford University Press, Oxford.; G. Nadathur, D. Miller, Higher-order logic programming, Handbook of Logic in AI and Logic Progamming, vol. 5, Oxford University Press, Oxford. · Zbl 0900.68129 |
| [114] | B. Nordström, K. Petersson, J. Smith, Programming in Martin-Löf’s Type Theory, An Introduction, Monographs on Computer Science, vol. 7, Oxford Press, Oxford, 1990.; B. Nordström, K. Petersson, J. Smith, Programming in Martin-Löf’s Type Theory, An Introduction, Monographs on Computer Science, vol. 7, Oxford Press, Oxford, 1990. · Zbl 0744.03029 |
| [115] | P.W. O’Hearn, Doubly closed categories, resource interpretations and the αλ-calculus, TLCA 99, to appear. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) ohearn.; P.W. O’Hearn, Doubly closed categories, resource interpretations and the αλ-calculus, TLCA 99, to appear. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) ohearn. |
| [116] | P.W. O’Hearn, D.J. Pym, The logic of bunched implications, Bull. Symbolic Logic (1999), to appear. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym.; P.W. O’Hearn, D.J. Pym, The logic of bunched implications, Bull. Symbolic Logic (1999), to appear. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym. · Zbl 0930.03095 |
| [117] | H. Ono, Substructural Logics, chapter Semantics for Substructural Logics, Oxford University Press, Oxford, 1993, pp. 259-291.; H. Ono, Substructural Logics, chapter Semantics for Substructural Logics, Oxford University Press, Oxford, 1993, pp. 259-291. · Zbl 0941.03522 |
| [118] | S. Owre, S. Rajan, J.M. Rushby, N. Shankar, M.K. Srivas, PVS: combining specification, proof checking, and model checking, in Computer-Aided Verification, CAV ’96, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, New Brunswick, NJ, July/August 1996, pp. 411-414.; S. Owre, S. Rajan, J.M. Rushby, N. Shankar, M.K. Srivas, PVS: combining specification, proof checking, and model checking, in Computer-Aided Verification, CAV ’96, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, New Brunswick, NJ, July/August 1996, pp. 411-414. |
| [119] | S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert, PVS Language Reference, Computer Science Laboratory, SRI International, Menlo Park, CA, September 1998.; S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert, PVS Language Reference, Computer Science Laboratory, SRI International, Menlo Park, CA, September 1998. |
| [120] | C. Parant, Synthesizing proofs from programs in the calculus of inductive constructions, in Mathematics for Program Construction, MPC’95, Lecture Notes in Computer Science, vol. 947, Springer, Berlin, Kloster Irsee, Germany, July 1995, pp. 351-379.; C. Parant, Synthesizing proofs from programs in the calculus of inductive constructions, in Mathematics for Program Construction, MPC’95, Lecture Notes in Computer Science, vol. 947, Springer, Berlin, Kloster Irsee, Germany, July 1995, pp. 351-379. |
| [121] | R. Paré, D. Schumacher, Abstract Families and the Adjoint Functor Theorems, Lecture Notes in Mathematics, vol. 661, Springer, Berlin, 1978, pp. 1-125.; R. Paré, D. Schumacher, Abstract Families and the Adjoint Functor Theorems, Lecture Notes in Mathematics, vol. 661, Springer, Berlin, 1978, pp. 1-125. · Zbl 0389.18002 |
| [122] | M. Parigot, Programming with proofs: a second order type theory, in European Symp. On Programming 88, Lecture Notes in Computer Science, vol. 300, Nancy, France, Springer, Berlin, March 1988, pp. 145-159.; M. Parigot, Programming with proofs: a second order type theory, in European Symp. On Programming 88, Lecture Notes in Computer Science, vol. 300, Nancy, France, Springer, Berlin, March 1988, pp. 145-159. |
| [123] | M. Parigot, Free deduction: an analysis of computations in classical logic, in 1st and 2nd Russian Conf. on Logic Programming, Lecture Notes in Artificial Intelligence, vol. 592, St. Petersburg, Russia, July 1991, pp. 361-380.; M. Parigot, Free deduction: an analysis of computations in classical logic, in 1st and 2nd Russian Conf. on Logic Programming, Lecture Notes in Artificial Intelligence, vol. 592, St. Petersburg, Russia, July 1991, pp. 361-380. · Zbl 0925.03203 |
| [124] | M. Parigot, \(λμ\)-calculus: an algorithmic interpretation of classical natural deduction, in LPAR’92, Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 190-201.; M. Parigot, \(λμ\)-calculus: an algorithmic interpretation of classical natural deduction, in LPAR’92, Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 624, St. Petersburg, Russia, July 1992, pp. 190-201. · Zbl 0925.03092 |
| [125] | Parigot, M., Recursive programming with proofs, Theoret. Comput. Sci., 94, 2, 335-356 (1992) · Zbl 0759.68014 |
| [126] | M. Parigot, Classical proofs as programs, in Computational Logic and Proof Theory, KGC’93, Lecture Notes in Computer Science, vol. 713, Springer, Berlin, Brno, Czech. Rep., August 1993, pp. 263-276.; M. Parigot, Classical proofs as programs, in Computational Logic and Proof Theory, KGC’93, Lecture Notes in Computer Science, vol. 713, Springer, Berlin, Brno, Czech. Rep., August 1993, pp. 263-276. · Zbl 0805.03012 |
| [127] | Paulin-Mohring, C.; Werner, B., Synthesis of ML programs in the system Coq, J. Symbolic Comput., (1993) (1915) |
| [128] | L.C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, Cambridge, 1987.; L.C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, Cambridge, 1987. · Zbl 0645.68041 |
| [129] | Paulson, L. C., The foundation of a generic theorem prover, J. Automat. Reason., 5, 363-397 (1989) · Zbl 0679.68173 |
| [130] | L.C. Paulson, Logic and Computer Science, chapter The next 700 theorem provers, Academic Press, New York, 1990.; L.C. Paulson, Logic and Computer Science, chapter The next 700 theorem provers, Academic Press, New York, 1990. |
| [131] | L.C. Paulson, Isabelle: a Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828, Springer, Berlin, 1994.; L.C. Paulson, Isabelle: a Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828, Springer, Berlin, 1994. · Zbl 0825.68059 |
| [132] | F. Pfenning, Logical Frameworks, chapter Logic Programming in the LF Logic Framework, Cambridge University Press, Cambridge, 1991, pp. 149-181.; F. Pfenning, Logical Frameworks, chapter Logic Programming in the LF Logic Framework, Cambridge University Press, Cambridge, 1991, pp. 149-181. · Zbl 0760.68014 |
| [133] | F. Pfenning, E. Rohwedder, Implementing the meta-theory of deductive systems, in: 11th Internat. Conf. on Automated Deduction, CADE-11, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, New York, June 1992, pp. 537-551.; F. Pfenning, E. Rohwedder, Implementing the meta-theory of deductive systems, in: 11th Internat. Conf. on Automated Deduction, CADE-11, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, New York, June 1992, pp. 537-551. · Zbl 0925.03062 |
| [134] | L. Pinto, Cut formulae and logic programming, in: 4th Internat. Workshop on Extensions of Logic Programming, Lecture Notes in Computer Science, vol. 798, Springer, Berlin, St Andrews, U.K., April 1993, pp. 282-300.; L. Pinto, Cut formulae and logic programming, in: 4th Internat. Workshop on Extensions of Logic Programming, Lecture Notes in Computer Science, vol. 798, Springer, Berlin, St Andrews, U.K., April 1993, pp. 282-300. |
| [135] | L. Pinto, R. Dyckhoff, A constructive type system to integrate logic and functional programming, in: D. Galmiche, L. Wallen (Eds.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Nancy, France, 1994, pp. 70-81.; L. Pinto, R. Dyckhoff, A constructive type system to integrate logic and functional programming, in: D. Galmiche, L. Wallen (Eds.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Nancy, France, 1994, pp. 70-81. |
| [136] | L. Pinto, R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic, in: Behara et al. (Eds.), Symposia Gaussiana, 1995, pp. 225-232.; L. Pinto, R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic, in: Behara et al. (Eds.), Symposia Gaussiana, 1995, pp. 225-232. · Zbl 0848.03002 |
| [137] | L. Pinto, R. Dyckhoff, Sequent calculi for the normal terms of the λΠ- and λΠΣ-calculi, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Lindau, Germany, 1998, pp. 93-106.; L. Pinto, R. Dyckhoff, Sequent calculi for the normal terms of the λΠ- and λΠΣ-calculi, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, Lindau, Germany, 1998, pp. 93-106. · Zbl 0917.68198 |
| [138] | A. Pitts, Categorical logic, in: S. Abramsky, D. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, vol. 6, Oxford University Press, Oxford, 1992, pp. 264-275.; A. Pitts, Categorical logic, in: S. Abramsky, D. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, vol. 6, Oxford University Press, Oxford, 1992, pp. 264-275. |
| [139] | D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almquist and Wiksell, Stockholm, 1965.; D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almquist and Wiksell, Stockholm, 1965. · Zbl 0173.00205 |
| [140] | Pym, D., A note [on] the proof theory of the λΠ-calculus, Stud. Logica, 54, 175-207 (1995) |
| [141] | D. Pym, A note on representation and semantics in logical frameworks. in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, New Brunswick, USA, 1996, pp. 101-108.; D. Pym, A note on representation and semantics in logical frameworks. in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, New Brunswick, USA, 1996, pp. 101-108. |
| [142] | Pym, D.; Harland, J., A uniform proof-theoretic investigation of linear logic programming, J. Logic Comput., 4, 2, 175-207 (1994) · Zbl 0797.03054 |
| [143] | D. Pym, L. Wallen, Logical Frameworks, chapter Proof-Search in the λΠ-Calculus, Cambridge University Press, Cambridge, 1991, pp. 283-294.; D. Pym, L. Wallen, Logical Frameworks, chapter Proof-Search in the λΠ-Calculus, Cambridge University Press, Cambridge, 1991, pp. 283-294. · Zbl 0753.03008 |
| [144] | D.J. Pym, Functorial Kripke-Beth-Joyal models of the λΠ-calculus I: type theory and internal logic, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication.; D.J. Pym, Functorial Kripke-Beth-Joyal models of the λΠ-calculus I: type theory and internal logic, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication. |
| [145] | D.J. Pym, Functorial Kripke-Beth-Joyal Models of the λΠ-calculus II: the LF logical framework, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication.; D.J. Pym, Functorial Kripke-Beth-Joyal Models of the λΠ-calculus II: the LF logical framework, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication. |
| [146] | D.J. Pym, Functorial Kripke-Beth-Joyal models of the λΠ-calculus III: logic programming and Its semantics, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication.; D.J. Pym, Functorial Kripke-Beth-Joyal models of the λΠ-calculus III: logic programming and Its semantics, 1999, in preparation. Note that [144], [145], [146] may appear within a single publication. |
| [147] | D.J. Pym, On bunched predicate logic, Proc. LICS, 1999, IEEE, New York, to appear: Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym.; D.J. Pym, On bunched predicate logic, Proc. LICS, 1999, IEEE, New York, to appear: Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym. |
| [148] | D.J. Pym, A relevant analysis of natural deduction, Lecture at EU Types Workshop, Baastad, Sweden.; D.J. Pym, A relevant analysis of natural deduction, Lecture at EU Types Workshop, Baastad, Sweden. |
| [149] | D.J. Pym, The semantics and proof theory of the logic of bunched implications, I: propositional BI, 1998. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym.; D.J. Pym, The semantics and proof theory of the logic of bunched implications, I: propositional BI, 1998. Available on the web at http://www.dcs.qmw.ac.uk \(/̃\) pym. |
| [150] | D.J. Pym, The semantics and proof theory of the logic of bunched implications, II: predicate BI, 1999, in preparation.; D.J. Pym, The semantics and proof theory of the logic of bunched implications, II: predicate BI, 1999, in preparation. |
| [151] | D.J. Pym, Proofs, search and computation in general logic, Ph.D. Thesis, University of Edinburgh, 1990. See also: Errata and Remarks, ECS-LFCS-93-265, University of Edinburgh, 1993.; D.J. Pym, Proofs, search and computation in general logic, Ph.D. Thesis, University of Edinburgh, 1990. See also: Errata and Remarks, ECS-LFCS-93-265, University of Edinburgh, 1993. |
| [152] | Pym, D. J., A unification algorithm for the λΠ-calculus, Internat. J. Found. Comput. Sci., 3, 2, 333-378 (1992) · Zbl 0784.03013 |
| [153] | D.J. Pym, Logic programming with bunched implications (extended abstract), Electronic Notes in Theoret. Comput. Sci. 17 (1998).; D.J. Pym, Logic programming with bunched implications (extended abstract), Electronic Notes in Theoret. Comput. Sci. 17 (1998). · Zbl 0917.68042 |
| [154] | E. Ritter, D.J. Pym, L.A. Wallen, On the intuitionistic force of classical search, in Proc. Tableaux 96, Lecture Notes in Computer Science, vol. 1071, Springer, Berlin, 1996, pp. 295-31.; E. Ritter, D.J. Pym, L.A. Wallen, On the intuitionistic force of classical search, in Proc. Tableaux 96, Lecture Notes in Computer Science, vol. 1071, Springer, Berlin, 1996, pp. 295-31. · Zbl 0952.03007 |
| [155] | E. Ritter, D.J. Pym, L.A. Wallen, Proof-terms for classical and intuitionistic resolution, in 13rd Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 1104, Springer, Berlin, 1996, pp. 17-31.; E. Ritter, D.J. Pym, L.A. Wallen, Proof-terms for classical and intuitionistic resolution, in 13rd Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 1104, Springer, Berlin, 1996, pp. 17-31. · Zbl 0958.03012 |
| [156] | Robinson, J. A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 23-41 (1965) · Zbl 0139.12303 |
| [157] | E. Rohwedder, Proof-search in the meta-theory of deductive systems, in: D. Galmiche, L. Wallen (Eds.), CADE Workshop on Proof-search in Type-theoretic Languages, Nancy, France, 1994, pp. 82-86.; E. Rohwedder, Proof-search in the meta-theory of deductive systems, in: D. Galmiche, L. Wallen (Eds.), CADE Workshop on Proof-search in Type-theoretic Languages, Nancy, France, 1994, pp. 82-86. |
| [158] | D.A. Schmidt, Denotational Semantics, Allyn & Bacon, Newton, MA, 1986.; D.A. Schmidt, Denotational Semantics, Allyn & Bacon, Newton, MA, 1986. |
| [159] | S. Schmitt, C. Kreitz, On transforming intuitionistic matrix proofs into standard sequent proofs, in: 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, vol. 918, St Goar am Rhein, Germany, Springer, Berlin, 1995, pp. 106-121.; S. Schmitt, C. Kreitz, On transforming intuitionistic matrix proofs into standard sequent proofs, in: 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, vol. 918, St Goar am Rhein, Germany, Springer, Berlin, 1995, pp. 106-121. |
| [160] | Seely, R. A.G., Hyperdoctrines, natural deduction and the Beck condition, Z. Math. Logik Grundlagen Math., 29, 505-542 (1983) · Zbl 0565.03032 |
| [161] | Smith, J., An interpretation of Martin-Löf’s type theory in a type fre theory of propositions, J. Symbolic Logic, 49, 3, 730-753 (1984) · Zbl 0618.03029 |
| [162] | A. Stoughton, Porgi: a proof-or-refutation generator for intuitionistic propositional logic, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, New Brunswick, USA, 1996, pp. 109-116.; A. Stoughton, Porgi: a proof-or-refutation generator for intuitionistic propositional logic, in: D. Galmiche (Ed.), CADE Workshop on Proof-Search in Type-Theoretic Languages, New Brunswick, USA, 1996, pp. 109-116. |
| [163] | Tammet, T., Proof strategies in linear logic, J. Automat. Reason., 12, 273-304 (1994) · Zbl 0821.03004 |
| [164] | T. Tammet, A resolution theorem prover for intuitionistic logic, in: 13th Internat. Conf. on Automated Deduction, CADE-13, Lecture Notes in Artificial Intelligence, vol. 1104, New Brunswick, NJ, USA, 1996, pp. 2-16.; T. Tammet, A resolution theorem prover for intuitionistic logic, in: 13th Internat. Conf. on Automated Deduction, CADE-13, Lecture Notes in Artificial Intelligence, vol. 1104, New Brunswick, NJ, USA, 1996, pp. 2-16. · Zbl 1412.68265 |
| [165] | A. Tarski, Logic, Semantics, Metamathematics, Clarendon Press, Oxford, 1956.; A. Tarski, Logic, Semantics, Metamathematics, Clarendon Press, Oxford, 1956. |
| [166] | A. Troelstra, Lectures on Linear Logic, CSLI, 1992.; A. Troelstra, Lectures on Linear Logic, CSLI, 1992. · Zbl 0942.03535 |
| [167] | T. Streicher, Correctness and completeness of a categorical semantics of the calculus of constructions, Ph.D. Thesis, Universität Passau, 1988.; T. Streicher, Correctness and completeness of a categorical semantics of the calculus of constructions, Ph.D. Thesis, Universität Passau, 1988. · Zbl 0684.03025 |
| [168] | A. Voronkov, Theorem proving in non-standard logics based on the inverse method, in: 11th Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, June 1992, pp. 648-662.; A. Voronkov, Theorem proving in non-standard logics based on the inverse method, in: 11th Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 607, Saratoga Springs, June 1992, pp. 648-662. · Zbl 0925.03075 |
| [169] | A. Voronkov, Proof-search in intuitionistic logic based on constraint satisfaction, in: 5th Internat. Workshop TABLEAUX’96, Lecture Notes in Artificial Intelligence, vol. 1071, Terrasini, Palermo, Italy, May 1996, pp. 312-327.; A. Voronkov, Proof-search in intuitionistic logic based on constraint satisfaction, in: 5th Internat. Workshop TABLEAUX’96, Lecture Notes in Artificial Intelligence, vol. 1071, Terrasini, Palermo, Italy, May 1996, pp. 312-327. · Zbl 1415.03010 |
| [170] | L.A. Wallen, Automated Proof Search in Non-Classical Logics, MIT Press, Cambridge, MA, 1990.; L.A. Wallen, Automated Proof Search in Non-Classical Logics, MIT Press, Cambridge, MA, 1990. · Zbl 0782.03003 |
| [171] | M. Winikoff, J. Harland, Implementing the linear logic programming language Lygon, in: J. Lloyd (Ed.), Proc. ILPS ’95, MIT Press, Cambridge, MA, 1995, p. 66.; M. Winikoff, J. Harland, Implementing the linear logic programming language Lygon, in: J. Lloyd (Ed.), Proc. ILPS ’95, MIT Press, Cambridge, MA, 1995, p. 66. |
| [172] | Yetter, D. N., Quantales and (noncommutative) linear logic, J. Symbolic Logic, 55, 1, 41-64 (1990) · Zbl 0701.03026 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
