natural language toolkit interface to the prover9 theorem prover c 20012023 nltk project dan garrette dhgarrettegmail com ewan klein ewaninf ed ac uk url https www nltk org for license information see license txt a theorem prover that makes use of the external prover9 package following is not yet used return code for 2 actually realized as 512 sos list exhausted a common base class used by both prover9command and macecommand which is responsible for maintaining a goal and a set of assumptions and generating prover9style input files from them print the list of the current assumptions a provercommand specific to the prover9 prover it contains the a printassumptions method that is used to print the list of assumptions in multiple formats param goal input expression to prove type goal sem expression param assumptions input expressions to use as assumptions in the proof type assumptions listsem expression param timeout number of seconds before timeout set to 0 for no timeout type timeout int param prover a prover if not set one will be created type prover prover9 see baseprovercommand decorateproof a common class extended by both prover9 and mace mace mace it contains the functionality required to convert nltkstyle expressions into prover9style expressions return the input string that should be provided to the prover9 binary this string is formed based on the goal assumptions and timeout value of this object a list of directories that should be searched for the prover9 executables this list is used by configprover9 when searching for the prover9 executables call the binary with the given input param inputstr a string whose contents are used as stdin param binary the location of the binary to call param args a list of commandline arguments return a tuple stdout returncode see configprover9 call prover9 via a subprocess convert a logic expression to prover9 format convert logic expression to prover9 formatted string the timeout value for prover9 if a proof can not be found in this amount of time then prover9 will return false use 0 for no timeout def proveself goalnone assumptionsnone verbosefalse if not assumptions assumptions stdout returncode self callprover9 self prover9inputgoal assumptions verboseverbose return returncode 0 stdout def prover9inputself goal assumptions s clearautodenials n only one proof required return s prover9parent prover9inputself goal assumptions def callprover9self inputstr args verbosefalse if self prover9bin is none self prover9bin self findbinaryprover9 verbose updatedinputstr if self timeout 0 updatedinputstr assignmaxseconds d nn self timeout updatedinputstr inputstr stdout returncode self call updatedinputstr self prover9bin args verbose if returncode not in 0 2 errormsgprefix error if errormsgprefix in stdout msgstart stdout indexerrormsgprefix errormsg stdoutmsgstart strip else errormsg none if returncode in 3 4 5 6 raise prover9limitexceededexceptionreturncode errormsg else raise prover9fatalexceptionreturncode errormsg return stdout returncode def callprooftransself inputstr args verbosefalse if self prooftransbin is none self prooftransbin self findbinaryprooftrans verbose return self callinputstr self prooftransbin args verbose class prover9exceptionexception def initself returncode message msg p9returncodesreturncode if message msg ns message exception initself msg class prover9fatalexceptionprover9exception pass class prover9limitexceededexceptionprover9exception pass tests and demos def testconfig a expression fromstringwalkj singj g expression fromstringwalkj p prover9commandg assumptionsa p executablepath none p prover9search p prove configprover9 usrlocalbin printp prove printp proof def testconverttoprover9expr for t in expr e expression fromstringt printconverttoprover9e def testprovearguments for goal assumptions in arguments g expression fromstringgoal alist expression fromstringa for a in assumptions p prover9commandg assumptionsalist prove for a in alist print s a printf g pn arguments manx not not manx not manx not manx manx not manx manx not manx manx manx not manx not manx manx not manx manx manx manx manx not manx not manx mortalsocrates all x manx mortalx mansocrates all x manx walksx mansocrates some y walksy all x manx all x manx some x all y seesx y some e3 walke3 subje3 mary some e1 seee1 subje1 john some e2 prede1 e2 walke2 subje2 mary some x e1 seee1 subje1 x some e2 prede1 e2 walke2 subje2 mary some e1 seee1 subje1 john some e2 prede1 e2 walke2 subje2 mary expressions rsome x y seesx y rsome x manx walksx rx manx walksx rx y seesx y rwalksjohn rx bigx y mousey rwalksx runsx threesx foursx rwalksx runsx rsome x prox seesjohn x rsome x manx not walksx rall x manx walksx def spacernum45 print num def demo printtesting configuration spacer testconfig print printtesting conversion to prover9 format spacer testconverttoprover9expressions print printtesting proofs spacer testprovearguments if name main demo natural language toolkit interface to the prover9 theorem prover c 2001 2023 nltk project dan garrette dhgarrette gmail com ewan klein ewan inf ed ac uk url https www nltk org for license information see license txt a theorem prover that makes use of the external prover9 package following is not yet used return code for 2 actually realized as 512 a fatal error occurred user s syntax error sos_empty prover9 ran out of things to do sos list exhausted the max_megs memory limit parameter was exceeded the max_seconds parameter was exceeded the max_given parameter was exceeded the max_kept parameter was exceeded a prover9 action terminated the search prover9 crashed most probably due to a bug a common base class used by both prover9command and macecommand which is responsible for maintaining a goal and a set of assumptions and generating prover9 style input files from them print the list of the current assumptions a provercommand specific to the prover9 prover it contains the a print_assumptions method that is used to print the list of assumptions in multiple formats param goal input expression to prove type goal sem expression param assumptions input expressions to use as assumptions in the proof type assumptions list sem expression param timeout number of seconds before timeout set to 0 for no timeout type timeout int param prover a prover if not set one will be created type prover prover9 see baseprovercommand decorate_proof a common class extended by both prover9 and mace mace mace it contains the functionality required to convert nltk style expressions into prover9 style expressions return the input string that should be provided to the prover9 binary this string is formed based on the goal assumptions and timeout value of this object a list of directories that should be searched for the prover9 executables this list is used by config_prover9 when searching for the prover9 executables call the binary with the given input param input_str a string whose contents are used as stdin param binary the location of the binary to call param args a list of command line arguments return a tuple stdout returncode see config_prover9 call prover9 via a subprocess convert a logic expression to prover9 format convert logic expression to prover9 formatted string the timeout value for prover9 if a proof can not be found in this amount of time then prover9 will return false use 0 for no timeout use prover9 to prove a theorem return a pair whose first element is a boolean indicating if the proof was successful i e returns value of 0 and whose second element is the output of the prover see prover9parent prover9_input only one proof required call the prover9 binary with the given input param input_str a string whose contents are used as stdin param args a list of command line arguments return a tuple stdout returncode see config_prover9 call the prooftrans binary with the given input param input_str a string whose contents are used as stdin param args a list of command line arguments return a tuple stdout returncode see config_prover9 tests and demos config_prover9 usr local bin test that parsing works ok try some proofs and exhibit the results
import os
import subprocess

import nltk
from nltk.inference.api import BaseProverCommand, Prover
from nltk.sem.logic import (
    AllExpression,
    AndExpression,
    EqualityExpression,
    ExistsExpression,
    Expression,
    IffExpression,
    ImpExpression,
    NegatedExpression,
    OrExpression,
)




p9_return_codes = {
    0: True,
    1: "(FATAL)",  
    2: False,  
    
    3: "(MAX_MEGS)",  
    4: "(MAX_SECONDS)",  
    5: "(MAX_GIVEN)",  
    6: "(MAX_KEPT)",  
    7: "(ACTION)",  
    101: "(SIGSEGV)",  
}


class Prover9CommandParent:
    

    def print_assumptions(self, output_format="nltk"):
        
        if output_format.lower() == "nltk":
            for a in self.assumptions():
                print(a)
        elif output_format.lower() == "prover9":
            for a in convert_to_prover9(self.assumptions()):
                print(a)
        else:
            raise NameError(
                "Unrecognized value for 'output_format': %s" % output_format
            )


class Prover9Command(Prover9CommandParent, BaseProverCommand):
    

    def __init__(self, goal=None, assumptions=None, timeout=60, prover=None):
        
        if not assumptions:
            assumptions = []

        if prover is not None:
            assert isinstance(prover, Prover9)
        else:
            prover = Prover9(timeout)

        BaseProverCommand.__init__(self, prover, goal, assumptions)

    def decorate_proof(self, proof_string, simplify=True):
        
        if simplify:
            return self._prover._call_prooftrans(proof_string, ["striplabels"])[
                0
            ].rstrip()
        else:
            return proof_string.rstrip()


class Prover9Parent:
    

    _binary_location = None

    def config_prover9(self, binary_location, verbose=False):
        if binary_location is None:
            self._binary_location = None
            self._prover9_bin = None
        else:
            name = "prover9"
            self._prover9_bin = nltk.internals.find_binary(
                name,
                path_to_bin=binary_location,
                env_vars=["PROVER9"],
                url="https://www.cs.unm.edu/~mccune/prover9/",
                binary_names=[name, name + ".exe"],
                verbose=verbose,
            )
            self._binary_location = self._prover9_bin.rsplit(os.path.sep, 1)

    def prover9_input(self, goal, assumptions):
        
        s = ""

        if assumptions:
            s += "formulas(assumptions).\n"
            for p9_assumption in convert_to_prover9(assumptions):
                s += "    %s.\n" % p9_assumption
            s += "end_of_list.\n\n"

        if goal:
            s += "formulas(goals).\n"
            s += "    %s.\n" % convert_to_prover9(goal)
            s += "end_of_list.\n\n"

        return s

    def binary_locations(self):
        
        return [
            "/usr/local/bin/prover9",
            "/usr/local/bin/prover9/bin",
            "/usr/local/bin",
            "/usr/bin",
            "/usr/local/prover9",
            "/usr/local/share/prover9",
        ]

    def _find_binary(self, name, verbose=False):
        binary_locations = self.binary_locations()
        if self._binary_location is not None:
            binary_locations += [self._binary_location]
        return nltk.internals.find_binary(
            name,
            searchpath=binary_locations,
            env_vars=["PROVER9"],
            url="https://www.cs.unm.edu/~mccune/prover9/",
            binary_names=[name, name + ".exe"],
            verbose=verbose,
        )

    def _call(self, input_str, binary, args=[], verbose=False):
        
        if verbose:
            print("Calling:", binary)
            print("Args:", args)
            print("Input:\n", input_str, "\n")

        
        cmd = [binary] + args
        try:
            input_str = input_str.encode("utf8")
        except AttributeError:
            pass
        p = subprocess.Popen(
            cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, stdin=subprocess.PIPE
        )
        (stdout, stderr) = p.communicate(input=input_str)

        if verbose:
            print("Return code:", p.returncode)
            if stdout:
                print("stdout:\n", stdout, "\n")
            if stderr:
                print("stderr:\n", stderr, "\n")

        return (stdout.decode("utf-8"), p.returncode)


def convert_to_prover9(input):
    
    if isinstance(input, list):
        result = []
        for s in input:
            try:
                result.append(_convert_to_prover9(s.simplify()))
            except:
                print("input %s cannot be converted to Prover9 input syntax" % input)
                raise
        return result
    else:
        try:
            return _convert_to_prover9(input.simplify())
        except:
            print("input %s cannot be converted to Prover9 input syntax" % input)
            raise


def _convert_to_prover9(expression):
    
    if isinstance(expression, ExistsExpression):
        return (
            "exists "
            + str(expression.variable)
            + " "
            + _convert_to_prover9(expression.term)
        )
    elif isinstance(expression, AllExpression):
        return (
            "all "
            + str(expression.variable)
            + " "
            + _convert_to_prover9(expression.term)
        )
    elif isinstance(expression, NegatedExpression):
        return "-(" + _convert_to_prover9(expression.term) + ")"
    elif isinstance(expression, AndExpression):
        return (
            "("
            + _convert_to_prover9(expression.first)
            + " & "
            + _convert_to_prover9(expression.second)
            + ")"
        )
    elif isinstance(expression, OrExpression):
        return (
            "("
            + _convert_to_prover9(expression.first)
            + " | "
            + _convert_to_prover9(expression.second)
            + ")"
        )
    elif isinstance(expression, ImpExpression):
        return (
            "("
            + _convert_to_prover9(expression.first)
            + " -> "
            + _convert_to_prover9(expression.second)
            + ")"
        )
    elif isinstance(expression, IffExpression):
        return (
            "("
            + _convert_to_prover9(expression.first)
            + " <-> "
            + _convert_to_prover9(expression.second)
            + ")"
        )
    elif isinstance(expression, EqualityExpression):
        return (
            "("
            + _convert_to_prover9(expression.first)
            + " = "
            + _convert_to_prover9(expression.second)
            + ")"
        )
    else:
        return str(expression)


class Prover9(Prover9Parent, Prover):
    _prover9_bin = None
    _prooftrans_bin = None

    def __init__(self, timeout=60):
        self._timeout = timeout
        

    def _prove(self, goal=None, assumptions=None, verbose=False):
        
        if not assumptions:
            assumptions = []

        stdout, returncode = self._call_prover9(
            self.prover9_input(goal, assumptions), verbose=verbose
        )
        return (returncode == 0, stdout)

    def prover9_input(self, goal, assumptions):
        
        s = "clear(auto_denials).\n"  
        return s + Prover9Parent.prover9_input(self, goal, assumptions)

    def _call_prover9(self, input_str, args=[], verbose=False):
        
        if self._prover9_bin is None:
            self._prover9_bin = self._find_binary("prover9", verbose)

        updated_input_str = ""
        if self._timeout > 0:
            updated_input_str += "assign(max_seconds, %d).\n\n" % self._timeout
        updated_input_str += input_str

        stdout, returncode = self._call(
            updated_input_str, self._prover9_bin, args, verbose
        )

        if returncode not in [0, 2]:
            errormsgprefix = "%%ERROR:"
            if errormsgprefix in stdout:
                msgstart = stdout.index(errormsgprefix)
                errormsg = stdout[msgstart:].strip()
            else:
                errormsg = None
            if returncode in [3, 4, 5, 6]:
                raise Prover9LimitExceededException(returncode, errormsg)
            else:
                raise Prover9FatalException(returncode, errormsg)

        return stdout, returncode

    def _call_prooftrans(self, input_str, args=[], verbose=False):
        
        if self._prooftrans_bin is None:
            self._prooftrans_bin = self._find_binary("prooftrans", verbose)

        return self._call(input_str, self._prooftrans_bin, args, verbose)


class Prover9Exception(Exception):
    def __init__(self, returncode, message):
        msg = p9_return_codes[returncode]
        if message:
            msg += "\n%s" % message
        Exception.__init__(self, msg)


class Prover9FatalException(Prover9Exception):
    pass


class Prover9LimitExceededException(Prover9Exception):
    pass







def test_config():

    a = Expression.fromstring("(walk(j) & sing(j))")
    g = Expression.fromstring("walk(j)")
    p = Prover9Command(g, assumptions=[a])
    p._executable_path = None
    p.prover9_search = []
    p.prove()
    
    print(p.prove())
    print(p.proof())


def test_convert_to_prover9(expr):
    
    for t in expr:
        e = Expression.fromstring(t)
        print(convert_to_prover9(e))


def test_prove(arguments):
    
    for (goal, assumptions) in arguments:
        g = Expression.fromstring(goal)
        alist = [Expression.fromstring(a) for a in assumptions]
        p = Prover9Command(g, assumptions=alist).prove()
        for a in alist:
            print("   %s" % a)
        print(f"|- {g}: {p}\n")


arguments = [
    ("(man(x) <-> (not (not man(x))))", []),
    ("(not (man(x) & (not man(x))))", []),
    ("(man(x) | (not man(x)))", []),
    ("(man(x) & (not man(x)))", []),
    ("(man(x) -> man(x))", []),
    ("(not (man(x) & (not man(x))))", []),
    ("(man(x) | (not man(x)))", []),
    ("(man(x) -> man(x))", []),
    ("(man(x) <-> man(x))", []),
    ("(not (man(x) <-> (not man(x))))", []),
    ("mortal(Socrates)", ["all x.(man(x) -> mortal(x))", "man(Socrates)"]),
    ("((all x.(man(x) -> walks(x)) & man(Socrates)) -> some y.walks(y))", []),
    ("(all x.man(x) -> all x.man(x))", []),
    ("some x.all y.sees(x,y)", []),
    (
        "some e3.(walk(e3) & subj(e3, mary))",
        [
            "some e1.(see(e1) & subj(e1, john) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))"
        ],
    ),
    (
        "some x e1.(see(e1) & subj(e1, x) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))",
        [
            "some e1.(see(e1) & subj(e1, john) & some e2.(pred(e1, e2) & walk(e2) & subj(e2, mary)))"
        ],
    ),
]

expressions = [
    r"some x y.sees(x,y)",
    r"some x.(man(x) & walks(x))",
    r"\x.(man(x) & walks(x))",
    r"\x y.sees(x,y)",
    r"walks(john)",
    r"\x.big(x, \y.mouse(y))",
    r"(walks(x) & (runs(x) & (threes(x) & fours(x))))",
    r"(walks(x) -> runs(x))",
    r"some x.(PRO(x) & sees(John, x))",
    r"some x.(man(x) & (not walks(x)))",
    r"all x.(man(x) -> walks(x))",
]


def spacer(num=45):
    print("-" * num)


def demo():
    print("Testing configuration")
    spacer()
    test_config()
    print()
    print("Testing conversion to Prover9 format")
    spacer()
    test_convert_to_prover9(expressions)
    print()
    print("Testing proofs")
    spacer()
    test_prove(arguments)


if __name__ == "__main__":
    demo()