The saturated tableaux for linear miniscope Horn-like temporal logic

DOI10.1007/BF00881951zbMath0814.03008MaRDI QIDQ1344880

Regimantas Pliuškevičius

Publication date: 22 February 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

automated deductiontableau systemsequent systemproof theory of linear temporal logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (3)

Finite sequent calculi for PLTL ⋮ Loop-type sequent calculi for temporal logic ⋮ Similarity saturation for first order linear temporal logic with UNLESS

Cites Work

• Sequential Calculus for a First Order Infinitary Temporal Logic
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The saturated tableaux for linear miniscope Horn-like temporal logic