Closed jparsert closed 6 years ago
No, formulas with free variables may be syntactically allowed but are not valid. See http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml: "In the THF, TFF, and FOF languages, every variable in a Formula must be bound by a preceding quantification with adequate scope".
What you can do is use cnf
instead of fof
, which will universally quantify all free variables. According to TPTP, cnf
is only for clauses, i.e. disjunctions of literals, but as a non-standard extension, Jukebox supports arbitrary formulas inside cnf
declarations.
Ah, thanks. Now I wonder though, in the jukebox library, is there a way, to read a line that has the form: fof(test, conjecture, ![X]: X) and print cnf(test,conjecture, ![X]: X)
You mean, to simply print cnf
instead of fof
but without otherwise doing anything to the problem? There is no way to do this currently. Can I ask what your use case is?
You can translate from FOF to CNF (by clausifying) with jukebox cnf
, and from CNF to FOF (by introducing quantifiers) with jukebox fof
.
By the way, the formula ![X]: X
is not valid TPTP because it is not allowed to quantify over Booleans (i.e. there are no Boolean variables). There is a proposal to add this to TPTP (see https://arxiv.org/abs/1505.01682) but it is not currently implemented in Jukebox. Is this something that you need?
My intention is essentially to create a file containing the sub-formulas of a given formula: so fof(x, conjecture, ![X] : ~predicate(X)) becomes 1: fof('', conjecture, ![X] : ~predicate(X)) 2: fof('', conjecture, ~ predicate(X)) 3: fof('', conjecture, predicate(X)) 4: fof('', conjecture, X) Now, I wanted to recursively do the same thing with 1-4, and create a list of sub-formulas of these formulas.
Clearly, the first step is easy. But now I obviously cannot parse the terms 1-4 anymore.
The first Idea I have for a solution, is essentially to transform free fariables to constants, I wonder if there is a function that replaces every occurrence of a term (Var X) with a term (Fun x). Well that's just substitution on terms. Which I see has been implemented.
Hey, So my current approach (which is good enough for my use) is to replace free variables by constants of the same name (but lowercase), which I am doing with the code pasted below. However, I have the problem that I don't really know how to use the renamer-type and I fear there is some hidden state carried over somewhere. Namely the exampe:
fof(myForms, conjecture, ![B]: p(B,c)).
produces the following two subformulas:
fof(myForms, conjecture, ![b]: p(b, c)). fof(myForms, conjecture, p(b, c)).
however, I want it to produce these two lines:
fof(myForms, conjecture, ![B]: p(B, c)). fof(myForms, conjecture, p(b, c)).
Looking into my code it seems like the p
added to the resulting list in this line:
subFormulas p@(ForAll b) = p : binder b
also changes when applying the substitution in line:
binder (Bind vars p) = subFormulas (subst (fromList . map getSubst $ toList vars) p)
Any idea what might cause this, and how to fix it?
`nameToLower (Fixed f) = Fixed $ fixedToLower f where fixedToLower (Basic s) = Basic . intern . map toLower $ unintern s fixedToLower = undefined nameToLower (Unique int s ren) = Unique int (map toLower s) ren nameToLower = undefined -- No idea what happens here, I dont think I need it.
binder (Bind vars p) = subFormulas (subst (fromList . map getSubst $ toList vars) p) where getSubst x = (x, nameToLower (name x) ::: (FunType [] O) :@: [])
subFormulas :: Form -> [Form]
subFormulas p@(Literal ) = [p]
subFormulas p@(Not f) = p : (subFormulas f)
subFormulas p@(And lst) = p : (concat $ map subFormulas lst)
subFormulas p@(Or lst) = p : (concat $ map subFormulas lst)
subFormulas p@(Equiv l r) = p : p : (subFormulas l) ++ (subFormulas r)
subFormulas p@(ForAll b) = p : binder b
subFormulas p@(Exists b) = p : binder b
subFormulas p@(Connective l r) = p : (subFormulas l) ++ (subFormulas r)
According to this BNF: http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#fof_plain_term
A formula with free variables is still valid. In particular the term "Variable" should be valid (please correct me if I am wrong). But the parser fails on a file containing the following line:
`fof(test, conjecture, Variable).´
FYI it also fails on more complex terms with predicates and free variables such as:
`fof(test, conjecture, ~P(Variable)).´