Source author record

Łukasz Czajka

Łukasz Czajka appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science math.LO

Catalog footprint

What is connected

4works

2topics

1close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2016arXiv

Goal Translation for a Hammer for Coq (Extended Abstract)

Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no hammers for such systems. We present an extension of the various hammer components to type theory: (i) a translation of a significant part of the Coq logic into the format of automated proof systems; (ii) a proof reconstruction mechanism based on a Ben-Yelles-type algorithm combined with limited rewriting, congruence closure and a first-order generalization of the left rules of Dyckhoff's system LJT.

preprint2016arXiv

Higher-order illative combinatory logic

We show a model construction for a system of higher-order illative combinatory logic $\mathcal{I}_ω$, thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system $\mathcal{I}_0$ of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

preprint2015arXiv

On the equivalence of different presentations of Turner's bracket abstraction algorithm

Turner's bracket abstraction algorithm is perhaps the most well-known improvement on simple bracket abstraction algorithms. It is also one of the most studied bracket abstraction algorithms. The definition of the algorithm in Turner's original paper is slightly ambiguous and it has been subject to different interpretations. It has been erroneously claimed in some papers that certain formulations of Turner's algorithm are equivalent. In this note we clarify the relationship between various presentations of Turner's algorithm and we show that some of them are in fact equivalent for translating lambda-terms in beta-normal form.

preprint2013arXiv

Partiality and Recursion in Higher-order Logic

We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system I_s allows for direct definitions of partial and general recursive functions, and provides means for handling functions whose termination has not been proven. We give examples of how properties of some recursive functions may be established in our system. In a technical appendix to the paper we prove consistency of I_s. The proof is by model construction. We then use this construction to show conservativity of I_s over classical first-order logic. Conservativity over higher-order logic is conjectured, but not proven.