9 citations · 14 across the 4 of their papers we have counts for
5 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…
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)…
Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
Boris Düdder, Oliver Garbe, Moritz Martens +2
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 type…
Retractions of Types with Many Atoms
Laurent Regnier, Pawel Urzyczyn
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-r…