A tableau proof system for a Mazurkiewicz trace logic with fixpoints

DOI10.1007/BFB0027421MaRDI QIDQ4610334zbMATH OpenOpenAlexFDO

Authors Peter Niebert, Barbara Sprick

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

atomic propositionmodel checkingproof systemtemporal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2086684
• scientific article; zbMATH DE number 1969331
• A tableau calculus for first-order branching time logic
• Publication:4864475
• scientific article; zbMATH DE number 1222573

Cites work

• A -calculus with local views for systems of sequential agents
• A partial approach to model checking
• Action refinement and property inheritance in systems of sequential agents
• An automata theoretic decision procedure for the propositional mu- calculus
• Automata for the modal -calculus and related results
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1318521 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• Results on the propositional \(\mu\)-calculus
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(2)

• A tableau style proof system for two paraconsistent logics
• Axiom Pinpointing in General Tableaux

This page was built for publication: A tableau proof system for a Mazurkiewicz trace logic with fixpoints

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