3 citations · 4 across the 7 of their papers we have counts for
9 papers
Between proof construction and SAT-solving
Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski
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 impli…
On non-structural subtype entailment
Aleksy Schubert
We prove that the non-structural subtype entailment problem for finite and regular type expressions is in PSPACE. In this way we close a decidability and complexity gap pending sin…
Formalisation of a frame stack semantics for a Java-like language
Aleksy Schubert, Jacek Chrząszcz
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally sp…
First-order answer set programming as constructive proof search
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…
On the Mints Hierarchy in First-Order Intuitionistic Logic
Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski
We stratify intuitionistic first-order logic over into fragments determined by the alternation of positive and negative occurrences of quantifiers (Mints hierarchy)…
Automata Theory Approach to Predicate Intuitionistic Logic
Maciej Zielenkiewicz, Aleksy Schubert
Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synt…