Automatic Proof Generation in Kleene Algebra

DOI10.1007/978-3-540-78913-0_28zbMATH Open1140.68042OpenAlexW1566154337MaRDI QIDQ3498428FDOQ3498428

Authors: J. Worthington 

Publication date: 15 May 2008

Published in: Relations and Kleene Algebra in Computer Science (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.651.6489

Recommendations

• On probabilistic Kleene algebras, automata and simulations
• On the coalgebraic theory of Kleene algebra with tests
• Kleene algebra with converse
• A cut-free cyclic proof system for Kleene algebra
• scientific article; zbMATH DE number 1688351

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Algebraic theory of languages and automata (68Q70) Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A completeness theorem for Kleene algebras and the algebra of regular events
• Title not available (Why is that?)
• On Hoare logic and Kleene algebra with tests
• Title not available (Why is that?)

Cited In (18)

• Automated Reasoning in Kleene Algebra
• Title not available (Why is that?)
• A bialgebraic approach to automata and formal language theory
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Automating Change of Representation for Proofs in Discrete Mathematics
• Algorithms for Kleene algebra with converse
• Title not available (Why is that?)
• Title not available (Why is that?)
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Left-handed completeness
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• On probabilistic Kleene algebras, automata and simulations
• Automating algebraic proof systems is NP-hard
• Title not available (Why is that?)
• Left-handed completeness
• Deciding Kleene algebra terms equivalence in Coq
• A Bialgebraic Approach to Automata and Formal Language Theory
• A cut-free cyclic proof system for Kleene algebra

This page was built for publication: Automatic Proof Generation in Kleene Algebra

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