Zobrazeno 1 - 10
of 67
pro vyhledávání: '"Paweł Urzyczyn"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 12, Issue 4 (2017)
We stratify intuitionistic first-order logic over $(\forall,\to)$ into fragments determined by the alternation of positive and negative occurrences of quantifiers (Mints hierarchy). We study the decidability and complexity of these fragments. We pro
Externí odkaz:
https://doaj.org/article/85990d3fc5b740598690898a1f8c904c
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 121, Iss Proc. ITRS 2012, Pp 18-34 (2013)
We describe ongoing work on a framework for automatic composition synthesis from a repository of software components. This work is based on combinatory logic with intersection types. The idea is that components are modeled as typed combinators, and a
Externí odkaz:
https://doaj.org/article/dc61de5bcb454f4f957e0e0d2d2a76d3
Autor:
Morten Heine Sørensen, Pawel Urzyczyn
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambd
Autor:
Andrej Dudenhefner, Paweł Urzyczyn
Publikováno v:
ACM Transactions on Computational Logic. 22:1-16
We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::346d563a529a04685227fef6d4de197e
https://doi.org/10.1145/3453481
https://doi.org/10.1145/3453481
Publikováno v:
ACM Transactions on Computational Logic. 17:1-29
We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co- 2-N exptime . Our approach is to represent proof-search as computation of an alternating
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::733004d2f6260bd510ec85a7676e6911
https://doi.org/10.1145/2981544
https://doi.org/10.1145/2981544
Autor:
Paweł Urzyczyn
Publikováno v:
Studia Logica. 104:957-1001
We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg's implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player, źros, is trying to construct a proof in normal form (positions in the ga
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6ed570899a9784355c8c914a8310813d
https://doi.org/10.1007/s11225-016-9661-4
https://doi.org/10.1007/s11225-016-9661-4
Autor:
Aleksy Schubert, Paweł Urzyczyn
We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Sigma_1 level of the Mints hiera
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::81727236588b54bd47410964f690dbb6
http://arxiv.org/abs/1804.10004
http://arxiv.org/abs/1804.10004
Autor:
Paweł Urzyczyn
Publikováno v:
Fundamenta Informaticae. 103:303-322
Is is shown that the inhabitation problem is decidable for intersection type assignment without the intersection elimination rule.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0cdd137fa63a47c81aebba396088f403
https://doi.org/10.3233/fi-2010-330
https://doi.org/10.3233/fi-2010-330
Autor:
Paweł Urzyczyn
Publikováno v:
Mathematical Structures in Computer Science. 13:5-13
The purpose of this note is to give a methodologically simple proof of the undecidability of strong normalisation in the pure lambda calculus. For this we show how to represent an arbitrary partial recursive function by a term whose application to an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::86a861eb143c69e2eaf71955fe66b8ff
https://doi.org/10.1017/s096012950200381x
https://doi.org/10.1017/s096012950200381x
Autor:
Paweł Urzyczyn, Jerzy Tiuryn
Publikováno v:
LICS
We prove that the subtyping problem induced by Mitchell's containment relation for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3e3cdc58ffe80e9fe729e9acd1f4d484
https://doi.org/10.1006/inco.2001.2950
https://doi.org/10.1006/inco.2001.2950