Package com.articulate.sigma.tp

package com.articulate.sigma.tp
  • Class
    Description
    ArityException
    Exception thrown when a formula has an incorrect arity for a predicate.
    ATPException
    Base exception class for all ATP (Automated Theorem Prover) related errors.
    ATPException.Builder
    Builder for constructing ATPException with full context
    ATPResult
    Generic result structure for ATP (Automated Theorem Prover) runs.
    ATPResult.Builder
    Builder for constructing ATPResult
    ECNF
     
    EProver
     
    ExecutableNotFoundException
    Exception thrown when an ATP executable (Vampire, EProver, LEO-III, etc.) is not found at the configured path or is not executable.
    FormulaTranslationException
    Exception thrown when a formula cannot be translated from SUO-KIF to a target format (TPTP, TFF, THF).
    GenPropFormulas
     
    GenPropFormulas.SZSonto
     
    LEO
    Class for invoking the latest version of LEO-III from Java.
    ProverCrashedException
    Exception thrown when an ATP process crashes or is killed by a signal.
    ProverTimeoutException
    Exception thrown when an ATP process times out.
    SZSExtractor
    Utility class for extracting SZS (TPTP Standard for System status values) information from prover output.
    SZSStatus
    Enumeration of SZS (TPTP Standard for System status values) statuses.
    SZSStatus.Category
    Category groupings for SZS statuses
    Vampire
    Class for invoking the latest research version of Vampire from Java A previous version invoked the KIF version of Vampire from Java but that's 15 years old now.
    Vampire.Logic
     
    Vampire.ModeType