Proof Search for the First-Order Connection Calculus in Maude | Zendy

Bjarne Holen | Zendy; Einar Broch Johnsen | Zendy; Arild Waaler | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Proof Search for the First-Order Connection Calculus in Maude

Author(s) -

Bjarne Holen,

Einar Broch Johnsen,

Arild Waaler

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.05.019

Subject(s) - rewriting , connection (principal bundle) , computer science , rule of inference , programming language , inference , layer (electronics) , theoretical computer science , algorithm , calculus (dental) , mathematics , artificial intelligence , medicine , chemistry , geometry , organic chemistry , dentistry

This paper develops a rewriting logic specification of the connection method for first-order logic, implemented in Maude. The connection method is a goal-directed proof procedure that requires a careful control over clause copies. The specification separates the inference rule layer from the rule application layer, and implements the latter at Maude's meta-level. This allows us to develop and compare different strategies for proof search

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research