Home
last modified time | relevance | path

Searched refs:FOOLParamodulation (Results 1 – 6 of 6) sorted by relevance

/dports/math/vampire/vampire-4.5.1/Inferences/
H A DFOOLParamodulation.hpp33 class FOOLParamodulation : public GeneratingInferenceEngine { class
35 CLASS_NAME(FOOLParamodulation);
36 USE_ALLOCATOR(FOOLParamodulation);
H A DFOOLParamodulation.cpp43 ClauseIterator FOOLParamodulation::generateClauses(Clause* premise) { in generateClauses()
/dports/math/vampire/vampire-4.5.1/Saturation/
H A DSaturationAlgorithm.cpp1480 if (opt.FOOLParamodulation()) { in createFromOptions()
1481 gie->addFront(new FOOLParamodulation()); in createFromOptions()
/dports/math/vampire/vampire-4.5.1/
H A DMakefile285 Inferences/FOOLParamodulation.o\
/dports/math/vampire/vampire-4.5.1/Shell/
H A DTheoryAxioms.cpp1156 if (env.options->FOOLParamodulation()) { in applyFOOL()
H A DOptions.hpp2095 bool FOOLParamodulation() const { return _FOOLParamodulation.actualValue; } in FOOLParamodulation() function in Shell::Options