Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

DOI10.1007/BF02358998MaRDI QIDQ1807462zbMATH OpenOpenAlexFDO

Authors R. Pliuškevičius

Publication date 22 November 1999

Published in Journal of Mathematical Sciences (New York) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02358998

zbMATH Keywords

decidabilityHorn-like sequentsinductive reasoninglinear temporal logicsaturated calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Logic in artificial intelligence (68T27)

Recommendations

• On the completeness and decidability of the Horn-like fragment of the first-order linear temporal logic
• scientific article; zbMATH DE number 782041
• scientific article; zbMATH DE number 517085

Cites work

• A complete axiomatic characterization of first-order temporal logic of linear time
• Concerning the semantic consequence relation in first-order temporal logic
• Decidability and incompleteness results for first-order temporal logics of linear time
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 1333594 (Why is no real title available?)
• scientific article; zbMATH DE number 517085 (Why is no real title available?)
• On the interpretability of arithmetic in temporal logic
• Sequential Calculus for a First Order Infinitary Temporal Logic

Cited in

(6)

• The saturated tableaux for linear miniscope Horn-like temporal logic
• On the completeness and decidability of the Horn-like fragment of the first-order linear temporal logic
• scientific article; zbMATH DE number 1678387 (Why is no real title available?)
• scientific article; zbMATH DE number 517085 (Why is no real title available?)
• scientific article; zbMATH DE number 782041 (Why is no real title available?)
• Saturation Up to Redundancy for Tableau and Sequent Calculi

This page was built for publication: Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1807462)