Lógica

On the undecidibility of type inhabitation for atomic polymorphism (part 2)

Por Clarence Protin (Independent Scholar).

Abstract: Pawel Urzyczyn has shown how to obtain a syntactic proof of the undecidability of type inhabitation for systems $F$ and $F_\omega$ by a reduction involving the codification of a certain undecidable $\forall,\rightarrow$- fragment of intutitionistic predicate calculus and the use of the Curry-Howard isomorphism. We show how this technique can be simplified and used to prove the undecidability of type inhabitation for atomic polymorphism.

Ler mais acerca de On the undecidibility of type inhabitation for atomic polymorphism (part 2)

On the undecidibility of type inhabitation for atomic polymorphism

Por Clarence Protin (Independent Scholar).

Abstract: Pawel Urzyczyn has shown how to obtain a syntactic proof of the undecidability of type inhabitation for systems $F$ and $F_\omega$ by a reduction involving the codification of a certain undecidable $\forall,\rightarrow$- fragment of intutitionistic predicate calculus and the use of the Curry-Howard isomorphism. We show how this technique can be simplified and used to prove the undecidability of type inhabitation for atomic polymorphism.

Ler mais acerca de On the undecidibility of type inhabitation for atomic polymorphism

On the elimination of arithmetical comprehension in proof mining (part 2)

Por Pedro Pinto (Universidade de Lisboa).

Ler mais acerca de On the elimination of arithmetical comprehension in proof mining (part 2)

On the elimination of arithmetical comprehension in proof mining

Por Pedro Pinto (Universidade de Lisboa).

Ler mais acerca de On the elimination of arithmetical comprehension in proof mining

Instantiation overflow from the viewpoint of categorical semantics and linear logic

Por Paolo Pistone (Università Roma Tre).

Ler mais acerca de Instantiation overflow from the viewpoint of categorical semantics and linear logic

A labeled logic for analyzing cyber-forensics evidence

Por Luca Viganò (King´s College London).

Ler mais acerca de A labeled logic for analyzing cyber-forensics evidence

Model theory and decidability theory for adele rings

Por Angus Macintyre (Queen Mary, University of London) (Emeritus).

Abstract: To each number field K there is attached a locally compact ring A_K, the ring of adeles over K. This ring is built from the completions of K at equivalence classes of absolute values. These can be either p-adic or real, or complex. Harmonic analysis on the adeles is a fundamental technique in number theory (since the famous thesis of John Tate) .

Ler mais acerca de Model theory and decidability theory for adele rings

Generic roots of exponential polynomials

Por Paola d'Aquino (Università Degli Study Della Campania).

Abstract: I will discuss the nature of the set of solutions of certain exponential polynomials over the complex field. This has connections with a conjecture due to Zilber on the axiomatization of the complex exponential field.