Skip to main content


A model guided instantiation heuristic for the superposition calculus with theories


Joshua Bax



Generalised Model Finding (GMF) is a quantifier instantiation heuristic for the su- perposition calculus in the presence of interpreted theories with arbitrarily quantified free function symbols ranging into theory sorts. The free function symbols are approximated by finite partial function graphs along with some simplifying assumptions which are iter- atively refined. Here we present an outline of the GMF approach, give an improvement that addresses some of these and then present some ideas for extending it with concepts from instantiation based theorem proving.

BibTeX Entry

    author           = {Bax, Joshua},
    month            = jul,
    year             = {2014},
    keywords         = {ssrg, vta},
    title            = {A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories},
    booktitle        = {Practical Aspects of Automated Reasoning workshop- IJCAR-14},
    pages            = {14},
    address          = {Vienna, Austria}