arXiv subjects

Lydia Kondylidou

Publications and source records attributed to Lydia Kondylidou.

2 recordsLinked to original sources

arXiv2026

The TPTP Format for Interpretations

This paper describes the TPTP format for representing interpretations. It provides a background survey that helped ensure that the representation format is adequate for different types of interpretations: Tarskian, Herbrand, and Kripke interpretations. The needs of applications that use models are considered. The syntax and semantics of the format are expounded in detail, with multiple examples. Verification of models is discussed. Some tools that support processing the format are noted. The properties of interpretations represented in the format are discussed.

cs.LO↗

arXiv2026

Tao's Equational Proof Challenge Accepted (Technical Report)

In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

cs.LO↗