Lines Matching defs:problem
1767 datatype problem =
1816 fun mkProblem {comments,includes,names,roles,problem} =
1820 val {axioms,conjecture} = problem
1839 {problem : Problem.problem,
1843 {problem = {axioms = [], conjecture = []},
1896 raise Error "TPTP problem has both cnf and fof conjecture formulas"
1908 val {problem,sources} : normalization = acc
1909 val {axioms,conjecture} = problem
1916 val problem = {axioms = axioms, conjecture = conjecture}
1919 {problem = problem,
1957 val {problem,sources} = norm
1958 val {axioms,conjecture} = problem
1959 val problem = {axioms = List.rev axioms, conjecture = List.rev conjecture}
1962 problem = problem,
2140 fun write {problem,mapping,filename} =
2142 val Problem {comments,includes,formulas} = problem
2162 val problem = {axioms = axioms, conjecture = conjecture}
2163 val resolution = Resolution.new Resolution.default problem
2172 val problem = read filename
2173 val problems = List.map #problem (normalize problem)
2531 fun fromProof {problem,proofs} =
2540 val Problem {formulas,...} = problem