Uses of Class
com.articulate.sigma.tp.Vampire
Packages that use Vampire
Package
Description
Provides classes for the Sigma knowledge engineering environment version developed
at Articulate Software Inc.
-
Uses of Vampire in com.articulate.sigma
Methods in com.articulate.sigma that return VampireModifier and TypeMethodDescriptionKB.askVampire(String suoKifFormula, int timeout, int maxAnswers) Submits a query to the inference engine.KB.askVampireForTQ(String suoKifFormula, int timeout, int maxAnswers, boolean modensPonens) KB.askVampireHOL(String stmt, int timeout, int maxAnswers, boolean useModals) Ask Vampire HOL using the existing.thf axioms. KB.askVampireModensPonens(String suoKifFormula, int timeout, int maxAnswers) STEPS: 1 - AskVampire to get the first output 2 - Process the output to keep only the authored axioms 3 - Send new command to vampire with Modens Ponens options 4 - If wanted drop the one premise formulas.KB.askVampireTHF(String test_path, int timeout, int maxAnswers) Executes the Vampire automated theorem prover with higher-order logic (HOL) mode on a given THF problem file.KB.askVampireTPTP(String test_path, int timeout, int maxAnswers) Executes a Vampire theorem prover query on a given TPTP problem file. -
Uses of Vampire in com.articulate.sigma.tp
Fields in com.articulate.sigma.tp declared as Vampire