Showing 1–5 of 5 results for author: Urzyczyn, P

Between proof construction and SAT-solving

Authors: Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski

Abstract: The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (wit… ▽ More The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (with all connectives) can be reduced to provability of implicational formulas of order three. Another advantage is a convenient interpretation in terms of simple alternating automata. Additionally, we distinguish some natural subclasses of IIPC corresponding to the complexity classes NP and co-NP. Our experimental results show that a simple decision procedure requires a significant amount of time only in a small fraction of cases. △ Less

Submitted 13 May, 2024; v1 submitted 9 May, 2024; originally announced May 2024.

First-order answer set programming as constructive proof search

Authors: Aleksy Schubert, Paweł Urzyczyn

Abstract: 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 hierarchy in first-order intuitionistic logic. It follows that Sigma_1 formulas using predicates of fixed arity (in particular unary) is of the same streng… ▽ More 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 hierarchy in first-order intuitionistic logic. It follows that Sigma_1 formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in Theory and Practice of Logic Programming △ Less

Submitted 30 April, 2018; v1 submitted 26 April, 2018; originally announced April 2018.

Comments: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX (arXiv:1804.10004)

On the Mints Hierarchy in First-Order Intuitionistic Logic

Authors: Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski

Abstract: 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 prove that even the $Δ_2$ level is undecidable and that $Σ_1$ is Expspace-complete. We also prove that the arity-bounded fragment of $Σ_1$ is complete f… ▽ More 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 prove that even the $Δ_2$ level is undecidable and that $Σ_1$ is Expspace-complete. We also prove that the arity-bounded fragment of $Σ_1$ is complete for co-Nexptime. △ Less

Submitted 27 December, 2016; v1 submitted 9 October, 2016; originally announced October 2016.

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2623

Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis

Authors: Boris Düdder, Oliver Garbe, Moritz Martens, Jakob Rehof, Paweł Urzyczyn

Abstract: 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 an algorithm for inhabitation {\textemdash} is there a combinatory term e with type tau relative to an environment Gamma? {\textemdash} can be used to… ▽ More 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 an algorithm for inhabitation {\textemdash} is there a combinatory term e with type tau relative to an environment Gamma? {\textemdash} can be used to synthesize compositions. Here, Gamma represents the repository in the form of typed combinators, tau specifies the synthesis goal, and e is the synthesized program. We illustrate our approach by examples, including an application to synthesis from GUI-components. △ Less

Submitted 30 July, 2013; originally announced July 2013.

Comments: In Proceedings ITRS 2012, arXiv:1307.7849

Journal ref: EPTCS 121, 2013, pp. 18-34

Retractions of Types with Many Atoms

Authors: Laurent Regnier, Pawel Urzyczyn

Abstract: We define a sound and complete proof system for affine beta-eta-retractions in simple types built over many atoms, and we state simple necessary conditions for arbitrary beta-eta-retractions in simple and polymorphic types. We define a sound and complete proof system for affine beta-eta-retractions in simple types built over many atoms, and we state simple necessary conditions for arbitrary beta-eta-retractions in simple and polymorphic types. △ Less

Submitted 5 December, 2002; originally announced December 2002.

Comments: First International Workshop on Isomorphisms of Types Toulouse, France, 8-9 november 2002

ACM Class: F.4.1