Connect++ 0.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
InferenceItem Struct Reference

Full representation of inferences, beyond just the name. More...

#include <InferenceItem.hpp>

Collaboration diagram for InferenceItem:
Collaboration graph
[legend]

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.
 

Detailed Description

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.

Constructor & Destructor Documentation

◆ InferenceItem()

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.


The documentation for this struct was generated from the following files: