Quelle tptp_isabelle Sprache: Lisp

#!/usr/bin/env bash
#
# Author: Jasmin Blanchette
# Author: Martin Desharnais-Schäfer
#
# DESCRIPTION: Isabelle tactics for TPTP competitive division

PRG="$(basename "$0")"

function usage() {
  echo
  echo "Usage: isabelle $PRG TIMEOUT FILES"
  echo
  echo " Runs a combination of Isabelle tactics on TPTP problems."
  echo " Each problem is allocated at most TIMEOUT seconds."
  echo
  exit 1
}

[ "$#" -eq 0 -o "$1" = "-?" ] && usage

SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
SCRATCH_FILE=/tmp/${SCRATCH}.thy

TIMEOUT=$1
shift

for FILE in "$@"
do
  echo "theory ${SCRATCH} imports \"HOL-TPTP.ATP_Problem_Import\" begin \
ML \<open> ATP_Problem_Import.isabelle_tptp_file @{theory} (${TIMEOUT}) \"${FILE}\" \<close> end" \
    > "${SCRATCH_FILE}"

  isabelle process_theories -O -U -l HOL-TPTP -f "${SCRATCH_FILE}" "${SCRATCH}" \
      | grep --line-buffered -vE \
          -e '^Running Draft ...$' \
          -e '^[[:space:]]*$' \
          -e '^Output $line [[:digit:]]+ of ".*"):$' \
          -e '^val it = \($: unit$' \
          -e '^Finished Draft $[0-9:]+ elapsed time(, [0-9:]+ cpu time, factor [0-9.]+)?$$' \
          -e '^PROOF FAILED for depth' \
          -e '^Failure node' \
          -e 'inferences so far. Searching to depth' \
          -e '^val ' \
          -e 'Loading theory' \
          -e '^poly.*warning: The type of' \
          -e '^ monotype.$'
done

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.