Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/Metis/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle problems2tptp.sml Sprache: SML

(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

open Useful;

(* ------------------------------------------------------------------------- *)
(* The program name.                                                         *)
(* ------------------------------------------------------------------------- *)

val PROGRAM = "problems2tptp";

(* ------------------------------------------------------------------------- *)
(* Problem data.                                                             *)
(* ------------------------------------------------------------------------- *)

use "problems.sml";

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

fun addSlash "" = ""
  | addSlash dir =
    if String.sub (dir, size dir - 1) = #"/" then dir
    else dir ^ "/";

fun checkProblems (problems : problem list) =
    let
      fun dups [] = ()
        | dups [_] = ()
        | dups (x :: (xs as x' :: _)) =
          if x <> x' then dups xs
          else raise Error ("duplicate problem name: " ^ x)

      val names = sort String.compare (List.map #name problems)
    in
      dups names
    end;

fun listProblem {name, comments = _, goal = _} = TextIO.print (name ^ "\n");

fun outputProblem outputDir {name,comments,goal} =
    let
      val filename = name ^ ".tptp"
      val filename =
          case outputDir of
            NONE => filename
          | SOME dir => addSlash dir ^ filename

      val comment_bar = nChars #"-" 77
      val comment_footer =
          ["TPTP file created by " ^ host () ^ " at " ^
           time () ^ " on " ^ date () ^ "."]
      val comments =
          [comment_bar] @
          ["Name: " ^ name] @
          (if List.null comments then [] else "" :: comments) @
          (if List.null comment_footer then [] else "" :: comment_footer) @
          [comment_bar]

      val includes = []

      val formulas =
          let
            val name = Tptp.FormulaName "goal"
            val role = Tptp.ConjectureRole
            val body = Tptp.FofFormulaBody (Formula.parse goal)
            val source = Tptp.NoFormulaSource
          in
            [Tptp.Formula
               {name = name,
                role = role,
                body = body,
                source = source}]
          end

      val problem =
          Tptp.Problem
            {comments = comments,
             includes = includes,
             formulas = formulas}

      val mapping = Tptp.defaultMapping

      val () =
          Tptp.write
            {problem = problem,
             mapping = mapping,
             filename = filename}
    in
      ()
    end;

(* ------------------------------------------------------------------------- *)
(* Program options.                                                          *)
(* ------------------------------------------------------------------------- *)

datatype mode = OutputMode | ListMode;

val MODE : mode ref = ref OutputMode;

val COLLECTION : string option ref = ref NONE;

val OUTPUT_DIRECTORY : string option ref = ref NONE;

local
  open Useful Options;
in
  val specialOptions =
      [{switches = ["--collection"], arguments = ["C"],
        description = "restrict to the problems in collection C",
        processor =
          beginOpt
            (stringOpt endOpt)
            (fn _ => fn c => COLLECTION := SOME c)},
       {switches = ["--list"], arguments = [],
        description = "just list the problems",
        processor = beginOpt endOpt (fn _ => MODE := ListMode)},
       {switches = ["--output-dir"], arguments = ["DIR"],
        description = "the output directory",
        processor =
          beginOpt
            (stringOpt endOpt)
            (fn _ => fn d => OUTPUT_DIRECTORY := SOME d)}];
end;

val VERSION = "1.0";

val versionString = PROGRAM^" v"^VERSION^"\n";

val programOptions =
    {name    = PROGRAM,
     version = versionString,
     header  = "usage: "^PROGRAM^" [option ...]\n" ^
               "Outputs the set of sample problems in TPTP format.\n",
     footer  = "",
     options = specialOptions @ Options.basicOptions};

fun succeed () = Options.succeed programOptions;
fun fail mesg = Options.fail programOptions mesg;
fun usage mesg = Options.usage programOptions mesg;

val (opts,work) =
    Options.processOptions programOptions (CommandLine.arguments ());

val () = if List.null work then () else usage "too many arguments";

(* ------------------------------------------------------------------------- *)
(* Top level.                                                                *)
(* ------------------------------------------------------------------------- *)

val () =
let
  val problems =
      case !COLLECTION of
        NONE => problems
      | SOME c => List.filter (isCollection c) problems

  val () = checkProblems problems

  val () =
      case !MODE of
        ListMode => app listProblem problems
      | OutputMode => app (outputProblem (!OUTPUT_DIRECTORY)) problems
in
  succeed ()
end
handle Error s => die (PROGRAM^" failed:\n" ^ s)
     | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.