A verified prover based on ordered resolution | Zendy

Anders Schlichtkrull | Zendy; Jasmin Christian Blanchette | Zendy; Dmitriy Traytel | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A verified prover based on ordered resolution

Author(s) -

Anders Schlichtkrull,

Jasmin Christian Blanchette,

Dmitriy Traytel

Publication year - 2019

Publication title -

hal (le centre pour la communication scientifique directe)

Language(s) - English

Resource type - Conference proceedings

ISBN - 978-1-4503-6222-1

DOI - 10.1145/3293880.3294100

Subject(s) - hol , soundness , nondeterministic algorithm , automated theorem proving , gas meter prover , computer science , resolution (logic) , completeness (order theory) , programming language , first order logic , axiom , functional programming , code (set theory) , algorithm , theoretical computer science , calculus (dental) , mathematical proof , mathematics , medicine , mathematical analysis , geometry , dentistry , set (abstract data type)

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

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