Bases: Solver
A solver that uses Prover9.
Prover9 is an automated theorem prover for first-order and equational logic
See The Prover9 site
Note that in order to use this integration, you need to install Prover9
and have it on your path.
Example:
>>> from typedlogic.integrations.solvers.prover9 import Prover9Solver
>>> from typedlogic.parsers.pyparser import PythonParser
>>> import tests.theorems.simple_contradiction as sc
>>> solver = Prover9Solver()
>>> solver.load(sc)
>>> r = solver.check()
>>> r.satisfiable
False
This solver does implements the open-world assumption.
Source code in src/typedlogic/integrations/solvers/prover9/prover9_solver.py
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82 | @dataclass
class Prover9Solver(Solver):
"""
A solver that uses Prover9.
Prover9 is an automated theorem prover for first-order and equational logic
See [The Prover9 site](https://www.cs.unm.edu/~mccune/prover9/)
Note that in order to use this integration, you need to [install Prover9](https://www.cs.unm.edu/~mccune/prover9/)
and have it on your path.
Example:
-------
>>> from typedlogic.integrations.solvers.prover9 import Prover9Solver
>>> from typedlogic.parsers.pyparser import PythonParser
>>> import tests.theorems.simple_contradiction as sc
>>> solver = Prover9Solver()
>>> solver.load(sc)
>>> r = solver.check()
>>> r.satisfiable
False
This solver does implements the open-world assumption.
"""
exec_name: str = field(default="prover9")
profile: ClassVar[Profile] = MixedProfile(Unrestricted(), OpenWorld())
def models(self) -> Iterator[Model]:
r = self.check()
if r.satisfiable:
yield Model()
def prove(self, sentence: Sentence) -> Optional[bool]:
proved = self._run(goals=[sentence])
return proved
def _run(self, goals: Optional[List[Sentence]] = None) -> bool:
compiler = Prover9Compiler()
# print(f"THEORY; n_sentences: {len(self.base_theory.sentences)}")
program = compiler.compile(self.base_theory, goals=goals)
# print(program)
with tempfile.NamedTemporaryFile(suffix=".prover9", mode="w") as fp:
fp.write(program)
fp.flush()
res = subprocess.run([self.exec_name, "-f", fp.name], capture_output=True)
if res.returncode not in (0, 2):
logger.error(res.stdout.decode())
raise ValueError(f"Prover9 failed with return code {res.returncode}")
if "THEOREM PROVED" in res.stdout.decode():
return True
else:
return False
def check(self) -> Solution:
proved = self._run()
unsat = not self.base_theory.goals and not proved
return Solution(satisfiable=unsat)
def dump(self) -> str:
compiler = Prover9Compiler()
return compiler.compile(self.base_theory)
|
