A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories | Zendy

Joshua Bax | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories

Author(s) -

Joshua Bax

Publication year - 2018

Publication title -

epic series in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2398-7340

DOI - 10.29007/b923

Subject(s) - heuristic , calculus (dental) , superposition principle , automated theorem proving , function (biology) , partial function , computer science , quantifier elimination , mathematics , algebra over a field , discrete mathematics , algorithm , mathematical optimization , pure mathematics , medicine , mathematical analysis , dentistry , evolutionary biology , biology

Generalised Model Finding (GMF) is a quantier instantiation heuristic for the superposition calculus in the presence of interpreted theories with nitely quantied free function symbols ranging into theory sorts. The free function symbols are approximated by nite partial function graphs along with simplifying assumptions which are iteratively rened. Here we present an outline of the GMF approach, give an improvement that addresses some eciency issues and then present some ideas for extending it with concepts from instantiation based theorem proving.

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