Bug in UTF8 Pretty Printer

[czengler]

Both

val a = "(![X]: p(X)) => p(a)".fol
val b = "![X]: p(X) => p(a)".fol

produce the same output with the UTF8 pretty printer.

[SHildebrandt]

Could it be the case that this is not an issue with the Pretty Printer but with the FOL TPTP Parser? To me it seems like

"![X]: p(X) => p(a)".fol

could be parsed to both

"(![X]: p(X)) => p(a)"

and

"![X]: (p(X) => p(a))"

I didn't look at the specification of PackratParsers in detail, so I might be wrong here, but I think that the problem is the ambiguity resulting from the methods quantifiedFormula and formula in fol.parsers.tptp.TPTPfofParser

[kuebler]

According to (http://en.wikipedia.org/wiki/First-order_logic#Notational_conventions), quantifiers should have higher precedence than implications, therefore ![X]: p(X) => p(a) should be interpreted as (![X]: p(X)) => p(a). In our implementation, equi- and antivalences bind less tight than implications which bind less tight than disjunctions which bind less tight than conjunctions which bind less tight than negations and finally quantifiers, therefore our implementation isn't exactly consistent with the precedence order at wikipedia (I think it was taken from P.B. Andrews: 'An Introduction to Mathematical Logic and Type Theory' but I'm not too sure about that).

[czengler]

"![X]: p(X) => p(a)"

is parsed to

"![X]: (p(X) => p(a))"

or equivalent:

FOLForAll(FOLVariable("X"), Implication(FOLPredicate("p", FOLVariable("X")), FOLPredicate("p", FOLFunction("a"))))

I think this is in accordance with the TPTP "standard" (and also e.g. Harrison's implementation). But we can discuss if this is the right behavior. But that is a parser issue.

The problem with the pretty printer remains. Once we decided on a precedence, we should fix that ;)

[SHildebrandt]

Possible solution for the parser issue: (keeping the current precedences and only checked on formula b) Change formula in line 80 of fol.parsers.tptp.TPTPfofParser to literal.

def quantifiedFormula: PackratParser[Formula[FOL]] = quantifier ~ variableList ~ ":" ~ literal ^^ {
    case `allQuant` ~ variables ~ ":" ~ lit => FOLForAll(Set(variables: _*), lit)
    case `exQuant` ~ variables ~ ":" ~ lit  => FOLExists(Set(variables: _*), lit)
  }

[kuebler]

Maybe the priority of quantifiers is defined erroneously. At least if I change the priority in Quantifier.scala to -50, I get the results I'd expect. I think Andrews defined the dot-operator (in our case the semicolon in the TPTP quantifier notation) to expand as far to the right as possible which would mean it has the least priority of all operators or am I getting something completely wrong?