3 papers
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…
cs.AI2025
On Deciding the Data Complexity of Answering Linear Monadic Datalog Queries with LTL Operators(Extended Version)
Alessandro Artale, Anton Gnatenko, Vladislav Ryzhikov +1
Our concern is the data complexity of answering linear monadic datalog queries whose atoms in the rule bodies can be prefixed by operators of linear temporal logic LTL. We first ob…