-
Notifications
You must be signed in to change notification settings - Fork 0
/
prover.py
22 lines (18 loc) · 1 KB
/
prover.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
# this is a simple theorem prover that uses the theorem map
import networkx as nx
# the theorem prover works by finding a path between nodes in the derivation graph (if possible)
# if a path is discovered, the theorems corresponding to each edge along the way can be applied
# they will by definition map from the desired premises to the desired conclusion
# produces a list of edge names that correspond to path from input node to output node
def findPath(G : nx.DiGraph, inputType : str, outputType : str) -> list[str]:
imports = [] # will store list of imports for the required theorems
theorems = [] # will store list of theorems in the order they must be applied
path = nx.astar_path(G, inputType, outputType)
# get the names of all theorems (edges) along the path
prevNode = path[0]
for node in path[1:]:
edge = G.get_edge_data(prevNode, node)
theorems.append(edge['objectName'])
imports.append(edge['importPath'])
prevNode = node
return imports, theorems