Lines Matching defs:problem
93 header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^
94 "Proves the input TPTP problem files.\n",
209 fun display_proof_body problem proofs =
217 {problem = problem,
232 {problem = proof,
240 fun display_proof filename problem proofs =
245 val () = display_proof_body problem proofs
259 val problem =
265 problem = {axioms = [],
270 (Tptp.freeVars problem)
273 {problem = problem,
302 val problem =
308 problem = cls}
312 (Tptp.freeVars problem)
317 {problem = problem,
367 val problem = Tptp.read {filename = filename, mapping = mapping}
369 val Tptp.Problem {comments,includes,formulas} = problem
371 if List.null includes then problem
437 val problem = {axioms = axioms, conjecture = conjecture}
439 val res = Resolution.new resolutionParameters problem
463 val {subgoal,problem,sources} = prob
465 val () = display_problem filename problem
469 case refute limit problem of
535 val () = if List.null work then usage "no input problem files" else ()