2 papers
cs.LO2026
Towards Weak Stratification for Logics of Definitions
Nathan Guermond
The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atom…
cs.LO2025
Ground Stratification for a Logic of Definitions with Induction
Nathan Guermond, Gopalan Nadathur
The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively…