Search

• < Previous
• 1
• Next >

---

Knowledge Spaces and the Completeness of Learning Strategies

Stefano Berardi ; Ugo de'Liguoro.

We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy.&nbsp;[&hellip;]

---

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

Federico Aschieri ; Stefano Berardi.

We apply to the semantics of Arithmetic the idea of ``finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee, \exists$) over a suitable structure $\StructureN$ for the&nbsp;[&hellip;]

---

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs

Stefano Berardi ; Makoto Tatsuta.

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in&nbsp;[&hellip;]

---