Non-monotonic Pre-fix Points and Learning

• Autorzy: Berardi S. , de’ Liguoro U.

Identyfikatory

DOI

10.3233/FI-2017-1470

• Języki publikacji: EN

Abstrakty

EN

We consider the problem of finding pre-fix points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interactive realizers are an abstract setting to represent learning processes, that can interpret non-constructive proofs. Atomic pieces of information of a knowledge space are stratified into levels, and evaluated into truth values depending on knowledge states. Realizers are then used to define operators that extend a given state by adding answers and possibly forcing us to remove some: in the learning process states of knowledge change non-monotonically. Existence of a pre-fix point of a realizer is equivalent to the termination of the learning process with some state of knowledge which is free of patent contradictions and such that there is nothing to add. In this paper we generalize our previous results in the case of level 2 knowledge spaces and deterministic operators to the case of ω-level knowledge spaces and of non-deterministic operators.

Słowa kluczowe

EN

knowledge space; one-level knowledge space; two-level knowledge space

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 3/4
• Strony: 259--280
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Berardi S.

• Computer Science Department, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy

autor

de’ Liguoro U.

• Computer Science Department, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy

Bibliografia

• [1] Coquand T. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 1995; 60 (1): 325- 337. doi: 10.2307/2275524.
• [2] Berardi S., de’Liguoro U. Toward the interpretation of non-constructive reasoning as non-monotonic learning. Information and Computation, 2009; 207 (1): 63-81. doi: 10.1016/j.ic.2008.10.003.
• [3] Aschieri F., Berardi S. Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. In: Proceedings of TLCA 2009, volume 5608 of SLNCS. 2009 pp. 20-34. doi: 10.1007/978-3-642-02273-9_4.
• [4] Berardi S., de’Liguoro U. Interactive realizers. A new approach to program extraction from non constructive proofs. ACM Transactions on Computational Logic, 2012; 13 (2). doi: 10.1145/2159531.2159533.
• [5] Berardi S, de’Liguoro U. Knowledge Spaces and Interactive Realizers. In: Proc. of CSL 2012, volume 16 of LIPICs. 2012 pp. 77-91. doi: 10.4230/LIPIcs.CSL.2012.77.
• [6] Aschieri F. Learning, Realizability and Games in Classical Arithmetic. Ph. d. thesis, University of Turin and Queen Mary University of London, 2010. arXiv: 1012.4992 [math.LO].
• [7] Berardi S., de’Liguoro U. Knowledge Spaces and the Completeness of Learning Strategies. Logical Methods in Computer Science, 2014; 10 (1): 1-23. doi: 10.2168/LMCS-10(1:9)2014.
• [8] Akama Y, Berardi S, Hayashi S, Kohlenbach U. An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In: Proc. of LICS’04. IEEE Computer Society, 2004 pp. 192-201. doi: 10.1109/lics.2004.1319613.
• [9] Stolzenberg G. Seeing Constructions. Conference given at Sophia Antipolis, Antibes, France, May 9, 1989.
• [10] Miller D. Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. In: 7th International Conference on Automated Deduction, volume 170 of SLNCS. 1984 pp. 375-393. doi: 10.1007/978-0-387-34768-4_22.
• [11] Buss SR. On Herbrand’s Theorem. In: Logic and Computational Complexity, International Workshop LCC ’94. 1994 pp. 195-209. doi: 10.1007/3-540-60178-3_85.
• [12] Mints G. Logic, Construction, Computation, chapter Non-Deterministic Epsilon Substitution Method for PA and ID1, pp. 325-342. Ontos-Verlag Series in Mathematical Logic. De Gruyter, 2012. URL http://www.degruyter.com/view/product/208943.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).