Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Descriptive Complexity in Lean: Completeness by First-Order Reductions
Pierre Senellart, Anton Gnatenko
We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around…
cs.LO2025
Analysing Temporal Reasoning in Description Logics Using Formal Grammars
Camille Bourgaux, Anton Gnatenko, Michaël Thomazo
We establish a correspondence between (fragments of) , a temporal extension of the description logic with the LTL operator , and…