Kevin Kappelmann

Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens et al.

Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic $λ$-calculus terms, as used in Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle/HOL. Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an LLM-powered AI agent independently produce pen-and-paper proofs, and the AI agent autoformalizes both in Isabelle, with further human-hinted AI interventions refining and generalizing the development.

Kevin Kappelmann

An important class of decidable first-order logic fragments are those satisfying a guardedness condition, such as the guarded fragment (GF). Usually, decidability for these logics is closely linked to the tree-like model property - the fact that satisfying models can be taken to have tree-like form. Decision procedures for the guarded fragment based on the tree-like model property are difficult to implement. An alternative approach, based on restricting first-order resolution, has been proposed, and this shows more promise from the point of view of implementation. In this work, we connect the tree-like model property of the guarded fragment with the resolution-based approach. We derive efficient resolution-based rewriting algorithms that solve the Quantifier-Free Query Answering Problem under Guarded Tuple Generating Dependencies (GTGDs) and Disjunctive Guarded Tuple Generating Dependencies (DisGTGDs). The Query Answering Problem for these classes subsumes many cases of GF satisfiability. Our algorithms, in addition to making the connection to the tree-like model property clear, give a natural account of the selection and ordering strategies used by resolution procedures for the guarded fragment. We also believe that our rewriting algorithm for the special case of GTGDs may prove itself valuable in practice as it does not require any Skolemisation step and its theoretical runtime outperforms those of known GF resolution procedures in case of fixed dependencies. Moreover, we show a novel normalisation procedure for the widely used chase procedure in case of (disjunctive) GTGDs, which could be useful for future studies.