# slomo/fol-2012

Merge branch 'master' of github.com:slomo/fol-2012

2 parents 3155590 + 07138e4 commit 95649af4185d1f8932cd3b7f18c58457c8968bab Marco Ziener committed Oct 12, 2012
Showing with 92 additions and 3 deletions.
1. +11 −2 resolution.py
2. +1 −1 resolution_test.py
3. +80 −0 tptp-test/MiamiDegree2.p
13 resolution.py
 @@ -78,7 +78,7 @@ def proof(formulas): # Phase 2 knf = splitted - iterations = 300 + iterations = 30 print("atomics",knf) @@ -98,7 +98,8 @@ def proof(formulas): return True knf.add(disj) - + print("Iteration",i) + print("Set",knf) return None # returns: <[]> @@ -217,6 +218,14 @@ def resolute(disj_a, disj_b): continue resolvente = Disjunction(list_disj_a + list_disj_b) + free_vars = disj_a.free_vars.union(disj_b.free_vars) + + #sig = {} + #for var in free_vars: + # sig[var] =next(gen_free()) + + #resolvente = Disjunction([ s_wrapper(x, sig) for x in resolvente ]) + #resolvente.free_vars = set(sig.values()) #if repr(list_disj_a) == "[~r(v4)]": # pdb.set_trace()
2 resolution_test.py
 @@ -5,7 +5,7 @@ def proof(formula): formula = o.transform(formula.negate()) - return r.proof(formula) + return r.proof([formula]) for_all = lambda v,x: Quantor("!", [ v ], x )
80 tptp-test/MiamiDegree2.p
 @@ -0,0 +1,80 @@ +fof(degree,axiom, + ( ( composition & humanities & science & math & social_science & language + & writing ) + => degree ) ). + +fof(composition,axiom, + ( ( eng105 & eng106 ) + => composition ) ). + +fof(composition_courses,axiom, + ( eng105 & eng106 ) ). + +fof(humanities,axiom, + ( ( art & literature & religion & phi115 ) + => humanities ) ). + +fof(art,axiom, + ( ( artXXX | arhXXX | danXXX | mcyXXX | thaXXX ) + => art ) ). + +fof(artXXX,axiom,artXXX ). + +fof(literature,axiom, + ( eng2XX + => literature ) ). + +fof(literature_courses,axiom, + ( eng2XX ) ). + +fof(religion,axiom, + ( relXXX + => religion ) ). + +fof(religion_courses,axiom, + ( relXXX ) ). + +fof(phi115,axiom, + ( phi115 ) ). + +fof(science,axiom, + ( ( bilXXX | chmXXX | ecsXXX | geoXXX | mscXXX | phyXXX ) + => science ) ). + +fof(phyXXX,axiom,phyXXX ). + +fof(math,axiom, + ( ( mth162 & ( cscXXX | staXXX) ) + => math ) ). + +fof(mth162,axiom,mth162 ). +fof(cscXXX,axiom,cscXXX ). + +fof(social_science,axiom, + ( ( apyXXX | ecoXXX | gegXXX | hisXXX | intXXX | polXXX | psyXXX | socXXX ) + => social_science ) ). + +fof(ecoXXX,axiom,ecoXXX ). + +fof(language,axiom, + ( ( arb2XX | chi2XX | fre2XX | ger2XX | gre2XX | heb2XX | ita2XX | jap2XX | + lat2XX | por2XX | spa2XX ) + => language ) ). + +fof(arbXXX,axiom,arb2XX ). + +fof(wwwXXX_writing,axiom, + wwwXXX => writing ). + +fof(wwwXXX,axiom,wwwXXX). + +fof(hisXXX_writing,axiom, + hisXXX => writing ). +fof(eng2XX_writing,axiom, + eng2XX => writing ). + +fof(phi115_writing,axiom, + phi115 => writing ). + +fof(get_degree,conjecture, + degree ).