Top

Published in:

2017 | OriginalPaper | Chapter

Automata Theory Approach to Predicate Intuitionistic Logic

Authors : Maciej Zielenkiewicz, Aleksy Schubert

Published in: Logic-Based Program Synthesis and Transformation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a program the type of which is a given formula. We present a model of automata that can handle proof construction in full intuitionistic first-order logic. The automata are constructed in such a way that any successful run corresponds directly to a normal proof in the logic. This makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Nominal Unification of Higher Order Expressions with Recursive Let

Note that a variable is a quasi-long proper eliminator because all arguments is an empty set in this case.

The name Arcadian automata stems from the fact that a slightly different and weaker notion of Eden automata was developed before [10] to deal with the fragment of the first-order intuitionistic logic with \(\forall \) and \(\rightarrow \) and in which the universal quantifier occurs only on positive positions.

Ben-Yelles, C.B.: Type-assignment in the lambda-calculus; syntax and semantics. Ph.D. thesis, Mathematics Department, University of Wales, Swansea, UK (1979)

Broda, S., Damas, L.: On long normal inhabitants of a type. J. Logic Comput. 15(3), 353–390 (2005)MathSciNetCrossRefMATH

Düdder, B., Martens, M., Rehof, J.: Staged composition synthesis. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 67–86. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_5 CrossRef

Filiot, E., Talbot, J., Tison, S.: Tree automata with global constraints. Int. J. Found. Comput. Sci. 21(4), 571–596 (2010)MathSciNetCrossRefMATH

de Groote, P.: On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Inf. Comput. 178(2), 441–464 (2002)MathSciNetCrossRefMATH

Hetzl, S.: Applying tree languages in proof theory. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 301–312. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28332-1_26 CrossRef

Prawitz, D.: Natural Deduction. Almqvist and Wiksell, Sweden (1965)MATH

Schubert, A., Dekkers, W., Barendregt, H.P.: Automata theoretic account of proof search. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). LIPIcs, vol. 41, pp. 128–143. Dagstuhl (2015)

Schubert, A., Urzyczyn, P., Zdanowski, K.: On the mints hierarchy in first-order intuitionistic logic. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 451–465. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46678-0_29 CrossRef

10.

Schubert, A., Urzyczyn, P., Walukiewicz-Chrzaszcz, D.: Restricted positive quantification is not elementary. In: Herbelin, H., Letouzey, P., Sozeau, M. (eds.) Proceedings of TYPES 2014. LIPIcs, vol. 39, pp. 251–273. Dagstuhl (2015)

11.

Takahashi, M., Akama, Y., Hirokawa, S.: Normal proofs and their grammar. Inf. Comput. 125(2), 144–153 (1996)MathSciNetCrossRefMATH

12.

Urzyczyn, P.: Intuitionistic games: determinacy, completeness, and normalization. Studia Logica 104(5), 957–1001 (2016). doi:10.1007/s11225-016-9661-4

Title: Automata Theory Approach to Predicate Intuitionistic Logic
Authors: Maciej Zielenkiewicz
Aleksy Schubert
Publisher: Springer International Publishing
Book: Logic-Based Program Synthesis and Transformation
Print ISBN: 978-3-319-63138-7

Electronic ISBN: 978-3-319-63139-4

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63139-4_20

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner