Connect++ 0.1
A fast, readable connection prover for first-order logic.
|
Full representation of inferences, beyond just the name. More...
#include <InferenceItem.hpp>
Public Member Functions | |
InferenceItem () | |
Constructor - probably unused. | |
InferenceItem (InferenceItemType) | |
Constructor - probably unused. | |
InferenceItem (InferenceItemType, ClauseNum) | |
Constructor - probably unused. | |
InferenceItem (InferenceItemType, const Literal &, LitNum) | |
Constructor - probably unused. | |
InferenceItem (InferenceItemType, const Literal &, LitNum, size_t) | |
Constructor for lemmata. | |
InferenceItem (InferenceItemType, const Literal &, LitNum, ClauseNum, LitNum, const Substitution &) | |
Constructor for extensions. | |
InferenceItem (InferenceItemType, const Literal &, LitNum, ClauseNum, LitNum, const Substitution &, size_t) | |
Constructor for reductions. | |
Public Attributes | |
InferenceItemType | T |
What kind of inference is this? | |
Literal | L |
The Literal that is used to make the inference. | |
LitNum | Lindex |
The index of the literal within the clause being used. | |
ClauseNum | C_2 |
For extensions, the number of the clause for which a fresh copy is being made. | |
LitNum | Lprime |
The index of the literal in C_2 being used. | |
Substitution | sigma |
A copy of the substitution that makes the rule applicable. | |
size_t | index_in_path |
The index in the path of the literal being usedd. | |
size_t | index_in_lemmata |
For certification, you want to know which element of the lemmata list was used when the Lemma rule was employed. | |
Full representation of inferences, beyond just the name.
The nomenclature here deliberately mimics that used in many of the publications describing the method, in an attempt to maintain readability.
As these are mostly used just to store information as the stack representing the proof is built, the methods are mostly just constructors.
InferenceItem::InferenceItem | ( | InferenceItemType | _T, |
const Literal & | _L, | ||
LitNum | _Lindex, | ||
size_t | _index_in_lemmata | ||
) |
Constructor for lemmata.
The last parameter is for index_in_lemmata.