################Automatic Theorem Prover####################
tempset=set([])
path=[]
def prove(start,target,h):
global tempset,path
if start==target:
return true
if h==0:
return false
for x in aviable_steps(start):
o=operate(start,x)
if not o in tempset: #efficient but could cause unprovabability in some rare cases
tempset.add(o)
if prove(o,target,h-1)==true:
path.append(start)
return true
return false
proved_already=set([])
def startprove(name,start,target,h,bRememberProved):
global tempset,path
path=[target]
if bRememberProved and (name,start,target) in proved_already:
return true
tempset=set([])
proved=prove(start,target,h)
path.reverse()
if bRememberProved and proved:
proved_already.add((name,start,target))
return proved
#######b can be deduced from a - system#####################
def aviable_steps(a):
global factli
av=[]
for x in factli:
if x[0]==a:
av.append(x[1])
return av
def operate(a,b):
return b
factli=[]
def Define(a,b):
factli.append((a,b))
######################hierachical text matching########################
def find_hierachical(In,patterns):
auswertung = {}
splits = (In+" ").split(" ")
len_splits = len(splits)
for j in xrange(len_splits-1,min(len_splits-1,1)-1,-1):
for k in range(len_splits+1):
parsIt = ""
for z in range(j):
if z + k >= len_splits:
break;
parsIt += splits[min(z+k, len(splits)-1)];
if z+1 != j:
parsIt+=" "
if parsIt != "" and parsIt!=" ":
for i in range(len(patterns)):
if parsIt in patterns[i]:
if not patterns[i] in auswertung.keys():
auswertung[patterns[i]] = j
else:
auswertung[patterns[i]] += j
return auswertung
def maxOf(result):
max=0
biggest=None
for x in result.keys():
if result[x]>max:
biggest=x
max=result[x]
return biggest
#######################Communication##############################
def validate(a):
return a.replace("?"," ")
def Communicate(a,b):
global commands
a=(" "+a+" ").replace(" a "," ") #easier parsing
commands=[x[0] for x in factli]
commands.extend([x[1] for x in factli])
commands.extend(["if then","has"])
cmd=maxOf(find_hierachical(a,commands))
if "if" in a and "then" in a:
Define(a.split("if")[1].split("then")[0],a.split("then")[1])
if "has" in a: #a has b?
v1=a.split("has")[0]
v2=a.split("has")[1]
if "?" in a:
v1=validate(v1)
v2=validate(v2)
a=maxOf(find_hierachical(v1,commands))
b=maxOf(find_hierachical(v2,commands))
return startprove("0",a,b,100,true)
else:
Define(v1,v2)
return cmd+"("+str(b)+")"
var('x')
#print startprove("0","auto","gummi",100,true)
def test(x):
return 2*x
print Communicate("a car has tires",None)
print Communicate("a tires has gummi",2*x)
print Communicate("a car has gummi?",None)
print factli
|
|
has(None)
tires (2*x)
True
[(' car ', ' tires '), (' tires ', ' gummi ')]
has(None)
tires (2*x)
True
[(' car ', ' tires '), (' tires ', ' gummi ')]
|