PN-matrices¶
Given a propositional signature \(\Sigma\), a PN-matrix over \(\Sigma\) is a structure \(\mathbb{M} = \langle \mathbf{M}, \{D_i\}_{i \in I} \rangle\), where \(\mathbf{M}\) is a multi-algebra over \(\Sigma\) and \(D_i \subseteq M\) is called a distinguished set, for each \(i \in I\).
In ct4l, we represent finite PN-matrices using the class
ct4l::PNMatrix, which holds a pointer to
a ct4l::MultiAlgebra object and
a vector of subsets of the carrier of the multi-algebra.
We also store internally the translation of such subsets to
the domain values.
When building a PN-matrix, you may specify whether you want the
constructor to compute the complements of each distinguished set
and store it as a distinguished set too. For example, if the carrier of the algebra is \(\{0,1\}\) and you
opt for this, then passing a vector having only the set \(\{1\}\)
will produce a PN-matrix with \(D_1 = \{1\}\) and
\(D_2 = \{0\}\). If the carrier of the algebra is \(\{0, 1, 2, 3\}\) and you give to the constructor a vector
with sets \(\{0, 1\}\) and \(\{0\}\), then, internally,
this vector will have four sets, in this sequence:
\(\{0, 1\}, \{2, 3\}, \{0\}, \{1, 2, 3\}\). This is intended to help
when we work with some notions of entailment associated to a PN-matrix.
Check ct4l::PNMatrix::PNMatrix() to see how to disable this option.
Note
Notice that the notion of PN-matrix we are using is a generalization of the usual one, which accepts only a single designated set. By taking a family, as we implemented, we can work more easily with many different notions of entailment, including two-dimensional (and \(n\)-dimensional) notions.
Example: Classical Logic matrix¶
Take the boolean algebra built in Example: Building the two-element Boolean algebra and assume we have a pointer to it stored in the variable algebra. The code below creates a PN-matrix based on such algebra:
ct4l::PNMatrix matrix {algebra, {{"T"}}};
API¶
-
template<typename
T>
classct4l::PNMatrix¶ Represents a non-deterministic matrix, allowing for empty sets in the interpretations, as well as multiple distinguished sets.
- Author
Vitor Greati
Public Functions
-
PNMatrix(decltype(_algebra) algebra, const std::vector<std::set<T>> &dsets_domain, bool make_complements = true)¶ Constructor that accepts the algebra, the dsets and a flat indicating whether the complement of each dset should be added as a dset.
In case the flag is true, for each i, dset[2i]=D_i and dset[2i+1]=V\D_i.
- Parameters
algebra: the pointer to the algebradsets: the designated sets in terms of the domain valuesmake_complements: indicates whether the complements of dsets should be computed
-
inline decltype(_dsets)
dsets() const¶ The distinguished sets in terms of the internal representation.
- Return
distinguished sets in internal representation
-
inline decltype(_dsets_domain)
dsets_domain() const¶ The distinguished sets in terms of the domain representation.
- Return
distinguished sets in domain representation
-
inline decltype(_algebra)
algebra() const¶ Return a pointer to the matrix algebra.
- Return
a pointer to the algebra