Proof Search for the First-Order Connection Calculus in Maude

DOI10.1016/J.ENTCS.2009.05.019MaRDI QIDQ5179137zbMATH OpenOpenAlexFDO

Authors Bjarne Holen, Einar Broch Johnsen, Arild Waaler

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.019

zbMATH Keywords

connection methodfirst-order logicMaudemeta-programmingreflectionrewriting logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Connection calculus theorem proving with multiple built-in theories
• MleanCoP: a connection prover for first-order modal logic
• Frontiers of Combining Systems
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 834568
• scientific article; zbMATH DE number 1348467
• -calculus model checking in Maude
• scientific article; zbMATH DE number 1882047
• M-calculus -- a sequent method for automatic theorem proving
• scientific article; zbMATH DE number 4170865

Cites work

• An approach to a systematic theorem proving procedure in first-order logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Conditional rewriting logic as a unified model of concurrency
• Connections in nonclassical logics
• Deduction, strategies, and rewriting
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• IeanCOP: lean connection-based theorem proving
• Maude: specification and programming in rewriting logic
• Reflection in conditional rewriting logic
• Refutations by Matings
• The tableaux work bench
• The TPTP problem library. CNF release v1. 2. 1

Describes a project that uses

Uses Software

• TPTP
• Maude
• LoTREC
• ileanCoP
• ITP

This page was built for publication: Proof Search for the First-Order Connection Calculus in Maude

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