3 problems

0 votes0 replies0 views
VETT as a foundation for a logic of ordered structures
The paper introduces VETT as a proof-relevant logic for formal category theory, with an extensional dependent type theory supporting categories, functors, profunctors, and natural…
Conjectureopencategory-theory formal-logic programming-languagesarXiv posted 2 days ago
0 votes0 replies0 views
Finite or ultimately periodic model conjecture for HyperLTL
Finite or ultimately periodic model conjecture. Every satisfiable HyperLTL formula has a model that consists of a finite set of traces, or an $\omega$ -regular set of traces, or at…
Conjectureopenformal-logic hyperproperties temporal-logicarXiv posted 2 days ago
0 votes0 replies0 views
Formalizability of nontrivial syntax-based mathematical algorithms in simple type theory with undefinedness
The logic ${\cal Q}^{\rm uqe}_{0}$ is a simple type theory with undefinedness, quotation, and evaluation. A syntax-based mathematical algorithm is a nontrivial mathematical algorit…
Conjectureopenautomated-reasoning formal-logic type-theoryarXiv posted 2 days ago

VETT as a foundation for a logic of ordered structures