This research has been supported by the italian Ministero della Pubblica Istruzione and by the CP Project of Honeywell Information System Italia.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E.W. Beth, Semantic Construction of Intuitionistic Logic. Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afb. Letterkunde, Nieuve Reeks, Deel 19, No. 11.
W. Bibel, Predicative Programming, Report of the Institut für Informatik, Technische Universität München, Munich, 1974.
C.L. Chang, R.C.T. Lee, Symbolic Logic and mechanical theorem proving (book), Academic Press Inc., New-York 1973.
R. Constable, Constructive Mathematics and automatic program writers, Proc. IFIP Congress 1971 (Lublijana), TA-2, North-Holland 1971.
G. Degli Antoni, P. Miglioli, M. Ornaghi, The synthesis of programs as an approach to the construction of reliable programs, Proc. of the International Conf. on proving and improving programs, Arc et Senans, July 1975, Huet, Kahn eds.
M.C. Fitting, Intuitionistic Logic, Model Theory and Forcing, (book), North-Holland 1969.
C. Goad, Computational uses of the manipulation of formal proofs, Stanford Dept. of Comp. Sci., Rep. n. STAN-CS-80-819, August 1980.
S. Goto, Program Synthesis from Natural Deduction Proofs, Int. Joint Conf. on Artificial Intelligence, Tokyo, 1979.
R. Kowalski, Logic for Problem Solving, (book), Elsevier North-Holland, 1979.
G. Kreisel, Some uses of proof-theory for finding computer programs, Notes for a talk in the Logical Symp. of Clermond-Ferrand, 1975, available as a manuscript.
S. Kripke, Semantical Analysis of Intuitionistic Logic I, in Formal Systems and Recursive Function, North-Holland, 1975.
P. Miglioli, M. Ornaghi, A purely logical computing model: the open proofs as programs, Istituto di Cibernetica dell'Università di Milano, internal rep. MIG 7, Sept. 1979.
P. Miglioli, M. Ornaghi, A logically justified model for non deterministic and parallel computations, Istituto di Cibernetica dell'Università di Milano, int. rep. MIG 8, 1978.
P. Miglioli, M. Ornaghi, Some models of computation from a unified proof-theoretical point of view (to appear).
U. Moscato, Intuizionismo e teoria della dimostrazione. Su un'estensione dei sistemi di refutazione aderente alla semantica dell'intuizionismo. Tesi di laurea, Università di Milano, A.A.1979/1980.
D. Prawitz, Natural deduction: a proof theoretical study, (book), Almqvist-Wiksell, 1965.
C.A. Smorynski, Applications of Kripke models, in S.A. Troelstra, Metamathematical investigation of Intuitionistic Arithmetic and Analysis, (book), Lect. Notes in Mathematics n.344, Springer-Verlag, 1973.
R. Smullyan, First order logic, (book), Springer, New York, 1968.
R. Statman, Intuitionistic propositional logic is polynomial-space complete, Theoretical Computer Science 9 (1979), North-Holland.
G. Bellin, Herbrand's theorem for calculi of sequents LK and LJ, Rep. of the University of Stockholm.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miglioli, P., Moscato, U., Ornaghi, M. (1981). Trees in Kripke models and in an intuitionistic refutation system. In: Astesiano, E., Böhm, C. (eds) CAAP '81. CAAP 1981. Lecture Notes in Computer Science, vol 112. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10828-9_72
Download citation
DOI: https://doi.org/10.1007/3-540-10828-9_72
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10828-3
Online ISBN: 978-3-540-38716-9
eBook Packages: Springer Book Archive