This page was written for an informal presentation at ADAM-2007.
formulas(assumptions). % "assumption" is a synonym for "sos" p(x) & p(i(x,y)) -> p(y) # label(condensed_detachment). subset(x,y) <-> (all z (member(z,x) -> member(z,y)) # label(subset_def). end_of_list.Example:
prover9 -f subset_trans.in > subset_trans.out
Previously: | x' ' ' ' = x |
Now: | x'''' = x |
op(400, infix, "--->").
op(333, postfix, @). op(333, prefix, ~). # not allowed, given the preceding declarationThis restriction avoids ambiguous strings, e.g., (~ x @).
tptp_to_ladr < PUZ031-1.p > PUZ031-1.in prover9 -f PUZ031-1.in > PUZ031-1.outIf you prefer, those two processes can be piped together:
tptp_to_ladr < PUZ031-1.p | prover9 > PUZ031-1.out2(Not all TPTP language features are supported.)
LADR to TPTP.
A Problem: TPTP accepts a smaller class of function/predicate symbols.
A Solution: Translator introduces new symbols when necessary.
ladr_to_tptp < RBA-2.in > RBA-2.p
A cycle of size 6:
% These are the default values assign(age_part, 1). % oldest clause assign(weight_part, 0). % lightest clause assign(true_part, 4). % lightest "true" clause assign(false_part, 4). % lightest "false" clause assign(random_part, 0). % random clause assign(hints_part, 2147483647). % lightest clause that matches a hintIf a clause for the current "part" is not available, that part is skipped.
FUTURE: A more general and flexible method is on the way (McCune, Kinyon, Veroff).
prover9 -f subset_trans_expand.in > subset_trans_expand.out
prover9 -f t2_23.in > t2_23.out (XML-formatted proof)
assign(max_depth, n). % analogous to max_weight assign(depth_penalty, n). % weight of clause C is increased by n * depth(C) assign(var_penalty, n). % weight of clause C is increased by n * number_of_vars(C)
prover9 -f subset_trans.in > subset_trans.out
prooftrans ivy -f subset_trans.out > subset_trans.ivy