Proof Search for the First-Order Connection Calculus in Maude

DOI10.1016/j.entcs.2009.05.019zbMath1347.68302OpenAlexW2036362080MaRDI QIDQ5179137

Arild Waaler, Bjarne Holen, Einar Broch Johnsen

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

reflectionfirst-order logicrewriting logicMaudemeta-programmingconnection method

Mathematics Subject Classification ID

Uses Software

• TPTP
• Maude
• LoTREC
• ileanCoP
• ITP

Cites Work

• Conditional rewriting logic as a unified model of concurrency
• The TPTP problem library. CNF release v1. 2. 1
• IeanCOP: lean connection-based theorem proving
• Maude: specification and programming in rewriting logic
• Reflection in conditional rewriting logic
• An approach to a systematic theorem proving procedure in first-order logic
• Deduction, Strategies, and Rewriting
• Refutations by Matings
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Unnamed Item
• Unnamed Item

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