A new first-order fixpoint logic, FL, is introduced as a Gentzen-type sequent calculus. FL is regarded as a generalization of the first-order linear-time temporal logic. The completeness and cut-elimination theorems for FL are proved using some theorems for embedding FL into infinitary logic. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Kamide, N. (2010). Completeness for generalized first-order LTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6359 LNAI, pp. 246–254). https://doi.org/10.1007/978-3-642-16111-7_28
Mendeley helps you to discover research relevant for your work.