Vampire automatic theorem prover for first-order classical logic.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
BlodKorv
CVS
Gematogen
VampireKernel
antlr
ANTLRException.cpp
ASTFactory.cpp
ASTRefCount.cpp
Atom.cpp
Atom.hpp
BaseAST.cpp
BitSet.cpp
Chain.hpp
CharBuffer.cpp
CharScanner.cpp
Clause.cpp
Clause.hpp
CommonAST.cpp
CommonToken.cpp
DLGLexer.cpp
DLexer.cpp
DLexerBase.cpp
Dump.cpp
Dump.hpp
Formula.cpp
Formula.hpp
Inference.cpp
Inference.hpp
InputBuffer.cpp
Int.cpp
Int.hpp
IntNameTable.cpp
IntNameTable.hpp
KIF.g
KIFLexer.cpp
KIFLexer.hpp
KIFLexerTokenTypes.hpp
KIFLexerTokenTypes.txt
KIFParser.cpp
KIFParser.hpp
LLkParser.cpp
LexerSharedInputState.cpp
List.hpp
ListSubstitution.cpp
ListSubstitution.hpp
Lists.hpp
Literal.cpp
Literal.hpp
Lst.hpp
Makefile.am
Makefile.in
Map.cpp
Map.hpp
Memory.cpp
Memory.hpp
Miniscope.cpp
Miniscope.hpp
MismatchedCharException.cpp
MismatchedTokenException.cpp
NoViableAltException.cpp
NoViableAltForCharException.cpp
Options.cpp
Options.hpp
Output.cpp
Output.hpp
Pair.hpp
Parser.cpp
ParserSharedInputState.cpp
Position.hpp
Problem.cpp
Problem.hpp
Query.cpp
Query.hpp
README
Random.cpp
Random.hpp
RecognitionException.cpp
Refutation.cpp
Refutation.hpp
Renaming.cpp
Renaming.hpp
Signature.cpp
Signature.hpp
Sort.hpp
Statistics.cpp
Statistics.hpp
String.cpp
Substitution.cpp
Substitution.hpp
SymCounter.cpp
SymCounter.hpp
TPTP.g
TPTPLexer.cpp
TPTPLexer.hpp
TPTPLexer.java
TPTPLexerTokenTypes.hpp
TPTPLexerTokenTypes.java
TPTPLexerTokenTypes.txt
TPTPParser.cpp
TPTPParser.hpp
TPTPParser.java
Tabulate.cpp
Tabulate.hpp
Term.cpp
Term.hpp
Token.cpp
TokenBuffer.cpp
TokenStreamSelector.cpp
Tracer.cpp
Tracer.hpp
Unit.cpp
Unit.hpp
Vampire.vpj
Vampire.vpw
Vampire.vpwhist
Vampire.vtg
VampireProofMacros.tex
Var.cpp
Var.hpp
XML.g
XMLLexer.cpp
XMLLexer.hpp
XMLLexerTokenTypes.hpp
XMLLexerTokenTypes.txt
XMLParser.cpp
XMLParser.hpp
assert.cpp
assert.hpp
client.pl
history
insert_lgpl
kif.cpp
lgpl.txt
makefile
primes.cpp
test.out
vampire.cpp
vampire.syntax

README

NOTICE: This software is LGPL v2.1 or later. Built on C++ and some Perl.

Peter Denno, 2004-07-12


These are instruction for building the "kif version" of Vampire under Linux, 
for use with the Sigma Knowledge Engineering Environment. 

PRELIMINARIES: You may need gcc 2.95.3. Other documentation on Vampire claims 
that this compiler is  necessary. It's what I used and it is believable that 
this version is necessary, because there are so many warnings generated during 
the compilation. 

When I compiled gcc, I used the configuration:   
  --prefix=/local --enable-threads --enable-languages=c++
If you have success with other versions of gcc, drop us a note at   
sigmakee-develop at lists.sourceforge.net.

TO BUILD:

1) edit the makefile in this directory and set CC to the path where you installed gcc 2.95.3
2) make 

Expect lots of errors, but expect it to produce and executable ./vampire

3) Set the following variable in the Sigma configuration to point to this executable
and directory. I built vampire in /local/sigma/current/Vampire, so I use:

<preference key="inferenceEngine" value="/local/sigma/current/Vampire/vampire"/>
<preference key="inferenceEngineDir" value="/local/sigma/current/Vampire/"/>

4) chmod 777 /local/sigma/current/Vampire/


n.b. Intermixed with Vampire files "proper" are files from the ANTLR-2.6.0 distribution.
This is the way Vampire is distributed. It isn't something particular to what
we are doing with Sigma. The antlr subdirectory of this directory is the same collection 
of files found in the antlr subdirectory of antlr-2.6.0. 

Note also that this distribution contains 12 files generated by ANTLR-2.6.0 
(the files {KIF,XML}*.{cpp,hpp,txt}). The parts of the makefile that create these
files have not been tested, and 'make clean' doesn't remove them.