modify conversion scripts

Author: kmineshima

scripts/convert_formulas.py

@@ -9,17 +9,24 @@
 
 from nltk.sem.drt import *
 from nltk2drs import convert_to_drs
-from nltk2normal import remove_true
+from nltk2normal import remove_true, rename
 from nltk2tptp import convert_to_tptp_proof
 from logic_parser import lexpr
 
 ARGS=None
 DOCS=None
 
 def get_formulas_from_xml(doc):
-    formulas = [s.get('sem', None) for s in doc.xpath(
-        './sentences/sentence/semantics[1]/span[1]')]
-    formulas = [f for f in formulas if f is not None]
+    formulas = []
+    for f in doc.xpath('./sentences/sentence'):
+        if f.xpath('semantics'):
+            s = f.xpath('semantics')[0]
+            if s.get('status') == 'success':
+                formulas += s.xpath('span[1]/@sem')
+            else:
+                formulas.append('semantics_error')
+        else:
+            formulas.append('syntax_error')
     return formulas
 
 def main(args = None):
@@ -38,14 +45,14 @@ def main(args = None):
     parser.add_argument("--format", nargs='?', type=str, default="drs",
         choices=["fol", "drs", "notrue", "drsbox", "tptp"],
         help="Output format (default: drs).")
-     
+
     ARGS = parser.parse_args()
 
     if not os.path.exists(ARGS.sem):
         print('File does not exist: {0}'.format(ARGS.sem), file=sys.stderr)
         parser.print_help(file=sys.stderr)
         sys.exit(1)
-    
+
     parser = etree.XMLParser(remove_blank_text=True)
     root = etree.parse(ARGS.sem, parser)
 
@@ -58,7 +65,7 @@ def main(args = None):
     if ARGS.format == "fol":
         results = [convert_to_drs(lexpr(formula)).fol() for formula in formulas]
     if ARGS.format == "notrue":
-        results = [remove_true(lexpr(formula)) for formula in formulas]
+        results = [rename(remove_true(lexpr(formula))) for formula in formulas]
     if ARGS.format == "tptp":
         inference = [lexpr(f) for f in formulas]
         results = convert_to_tptp_proof(inference)

scripts/nltk2drs.py

@@ -9,8 +9,8 @@
 dp = nltk.sem.DrtExpression.fromstring
 
 def convert_to_drs(expression):
-    expression = rename_variable(expression)
     expression = remove_true(expression)
+    expression = rename(expression)
     drs_expr = convert_drs(DRS([],[]), expression)
     return drs_expr
 

scripts/nltk2normal.py

@@ -6,7 +6,12 @@
 from nltk.internals import Counter
 from logic_parser import lexpr
 
-_counter = Counter()
+class NCounter(Counter):
+    def reset(self):
+        self._value = 0
+        return self._value
+
+_counter = NCounter()
 
 # Term t ::=
 #   x,y,z         <IndividualVariableExpression>
@@ -58,13 +63,16 @@ def new_variable(var):
     var = VariableExpression(var)
     # isinstance(var,EventVariableExpression) must come first
     if isinstance(var, EventVariableExpression):
-        prefix = 'e0'
+        prefix = 'e'
     elif isinstance(var, IndividualVariableExpression):
-        prefix = 'x0'
+        if str(var)[0] == 'd':
+            prefix = 'd'
+        else:
+            prefix = 'x'
     elif isinstance(var, FunctionVariableExpression):
-        prefix = 'F0'
+        prefix = 'F'
     else:
-        prefix = 'z0'
+        prefix = 'z'
     v = Variable("%s%s" % (prefix, _counter.get()))
     return v
 
@@ -291,6 +299,11 @@ def rename_variable(expression):
         expr = expression
     return expr
 
+def rename(f):
+    res = rename_variable(f)
+    _counter.reset()
+    return res
+
 def convert_to_prenex(expression):
     # Convert a formula to one where all existential quantifers come first.
     expression = remove_true(expression)
@@ -492,7 +505,6 @@ def normalize_symbols(expression):
 comp12 = lexpr(r'(exists x.(_boy(x) & True & exists e.(_walk(e) & (Subj(e) = x) & _slowly(e) & exists x.(_park(x) & True & _in(e,x) & True))) & exists x.(_girl(x) & True & exists e.(_walk(e) & (Subj(e) = x) & _slowly(e) & exists x.(_park(x) & True & _in(e,x) & True))))')
 comp13 = lexpr(r'exists x.(_walking(x) & _man(x) & True & exists e.((Subj(e) = Subj(e)) & True))')
 
-
 test = [v1,v2,v3,
         atom1,atom2,atom3,atom4,atom5,
         nonatom1,nonatom2,

scripts/nltk2tptp.py

@@ -2,27 +2,28 @@
 
 from nltk.sem.logic import *
 from logic_parser import lexpr
-from nltk2normal import rename_variable, remove_true
+from nltk2normal import rename_variable, remove_true, rename
 
 def convert_to_tptp_proof(formulas):
     if len(formulas) == 1:
         conjecture = formulas[0]
-        tptp_script = ['fof(h,conjecture,{0}).'.format(conjecture)]
+        tptp_script = ['tff(h,conjecture,{0}).'.format(conjecture)]
     else:
         premises, conjecture = formulas[:-1], formulas[-1]
         tptp_script = []
         num = 1
         for formula in premises:
             formula = convert_to_tptp(formula)
-            tptp_script.append('fof(t{0},axiom,{1}).'.format(num,formula))
+            tptp_script.append('tff(t{0},axiom,{1}).'.format(num,formula))
             num += 1
         conjecture = convert_to_tptp(conjecture)
-        tptp_script.append('fof(h,conjecture,{0}).'.format(conjecture))
-    return tptp_script        
+        tptp_script.append('tff(h,conjecture,{0}).'.format(conjecture))
+    return tptp_script
 
 def convert_to_tptp(expression):
-    expression = rename_variable(expression)
+    # expression = rename_variable(expression)
     expression = remove_true(expression)
+    expression = rename(expression)
     tptp_str = convert_tptp(expression)
     return tptp_str
 
@@ -106,13 +107,19 @@ def convert_tptp_not(expression):
 def convert_tptp_exists(expression):
     variable = convert_tptp(expression.variable).upper()
     term = convert_tptp(expression.term)
-    tptp_str = '?[' + variable + ']: ' + Tokens.OPEN + term + Tokens.CLOSE
+    if variable[0] == 'D':
+        tptp_str = '?[' + variable + ':$int]: ' + Tokens.OPEN + term + Tokens.CLOSE
+    else:
+        tptp_str = '?[' + variable + ']: ' + Tokens.OPEN + term + Tokens.CLOSE
     return tptp_str
 
 def convert_tptp_all(expression):
     variable = convert_tptp(expression.variable).upper()
     term = convert_tptp(expression.term)
-    tptp_str = '![' + variable + ']: ' + Tokens.OPEN + term + Tokens.CLOSE
+    if variable[0] == 'D':
+        tptp_str = '![' + variable + ':$int]: ' + Tokens.OPEN + term + Tokens.CLOSE
+    else:
+        tptp_str = '![' + variable + ']: ' + Tokens.OPEN + term + Tokens.CLOSE
     return tptp_str
 
 def convert_tptp_lambda(expression):