P 3
Emil Post
Emil Post's three-valued logic, with values T , F , and N . It features
a deviant negation that performs a cyclic shift in value.
Contents
Common labels for the values include:
T
1
just true
N
0.5
neither true nor false
F
0
just false
Designated Values
The set of designated values for P 3 T }
The value of a sentence with a truth-functional operator is determined by
the values of its operands according to the following tables.
Disjunction
∨
T
T
T
T
N
T
N
N
F
T
N
F
Defined Operators
Conjunction ∧ ¬ ∨
Given the behavior of ¬
Conjunction
∧
T
F
F
N
N
F
T
N
F
N
N
N
The Material Conditional ⊃
Likewise the Material Biconditional ≡ ⊃ ∧
A ≡ B \(:=\) (A ⊃ B) ∧ (B ⊃ A)
Material Conditional
⊃
T
T
N
N
N
T
N
F
F
T
T
T
Material Biconditional
≡
T
F
F
F
N
F
T
N
F
F
N
F
Compatibility Tables
P 3 Assertion or Conditional operators,
but we include tables and rules for them, for cross-compatibility.
Conditional
→
T
T
N
N
N
T
N
F
F
T
T
T
Biconditional
↔
T
F
F
F
N
F
T
N
F
F
N
F
A sentence with n -ary predicate \(P\) over parameters \(\langle a_0, ... ,a_n\rangle\)
has the value:
T iff \(\langle a_0, ... ,a_n\rangle\) is in the extension of \(P\)
and not in the anti-extension of \(P\) .
F iff \(\langle a_0, ... ,a_n\rangle\) is in the anti-extension of \(P\) and
not in the extension of \(P\) .
N iff \(\langle a_0, ... ,a_n\rangle\) is in neither the extension
nor the anti-extension of \(P\) .
Logical Consequence is defined in terms of the set of designated values
{ T }:
Logical Consequence
C is a Logical Consequence of A iff
all models where A has a desginated value
are models where C also has a designated value.
P 3 FDE .
Nodes for many-value tableaux consiste of a sentence plus a designation
marker: ⊕ for designated , and ⊖ for undesignated .
To build the trunk for an argument, add a designated node for each premise, and
an undesignated node for the conclusion.
To build the trunk for the argument A1 ... An ∴ B write:
In general, rules for connectives consist of four rules per connective:
a designated rule, an undesignated rule, a negated designated rule, and a negated
undesignated rule. The special case of negation has a total of two rules which apply
to double negation only, one designated rule, and one undesignated rule.
Operator Rules
¬ Rules
¬ ¬ ⊕ Double Negation Designated [source]
¬ ¬ ⊖ Double Negation Undesignated [source]
∧ Rules
∧ ⊕ Conjunction Designated [source]
A ∧ B ⊕
⋮
¬A ⊖
A ⊖
¬B ⊖
B ⊖
∧ ⊖ Conjunction Undesignated [source]
¬ ∧ ⊕ Conjunction Negated Designated [source]
¬ ∧ ⊖ Conjunction Negated Undesignated [source]
⊃ Rules
⊃ ⊕ Material Conditional Designated [source]
⊃ ⊖ Material Conditional Undesignated [source]
¬ ⊃ ⊕ Material Conditional Negated Designated [source]
¬ ⊃ ⊖ Material Conditional Negated Undesignated [source]
≡ Rules
≡ ⊕ Material Biconditional Designated [source]
A ≡ B ⊕
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊕
≡ ⊖ Material Biconditional Undesignated [source]
A ≡ B ⊖
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊖
¬ ≡ ⊕ Material Biconditional Negated Designated [source]
¬(A ≡ B) ⊕
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊕
¬ ≡ ⊖ Material Biconditional Negated Undesignated [source]
¬(A ≡ B) ⊖
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊖
Compatibility Rules
→ Rules
→ ⊕ Conditional Designated [source]
→ ⊖ Conditional Undesignated [source]
¬ → ⊕ Conditional Negated Designated [source]
¬ → ⊖ Conditional Negated Undesignated [source]
↔ Rules
↔ ⊕ Biconditional Designated [source]
A ↔ B ⊕
⋮
(A → B) ∧ (B → A) ⊕
↔ ⊖ Biconditional Undesignated [source]
A ↔ B ⊖
⋮
(A → B) ∧ (B → A) ⊖
¬ ↔ ⊕ Biconditional Negated Designated [source]
¬(A ↔ B) ⊕
⋮
¬((A → B) ∧ (B → A)) ⊕
¬ ↔ ⊖ Biconditional Negated Undesignated [source]
¬(A ↔ B) ⊖
⋮
¬((A → B) ∧ (B → A)) ⊖
class Rules [source]
closure : tuple [ type [ ClosingRule ] , ... ] = (<class 'pytableaux.logics.k3.Rules.GlutClosure'>, <class 'pytableaux.logics.fde.Rules.DesignationClosure'>)
class DoubleNegationDesignated ( tableau / ** opts ) [source]
From an unticked, designated, double-negation node n on a branch b ,
add two undesignated nodes to b , one with the double-negatum, and one
with the negatum. Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Negation(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Negation(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Negation), (Legend.designation, True))
The rule class legend.
name : str = 'DoubleNegationDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (20, 1)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class DoubleNegationUndesignated ( tableau / ** opts ) [source]
From an unticked, undesignated, double-negation node n on a branch b ,
make two branches b' and b'' from b . On b' add a designated
node with the negatum, and on b' add a designated node with the
double-negatum. Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Negation(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Negation(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 1
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Negation), (Legend.designation, False))
The rule class legend.
name : str = 'DoubleNegationUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (20, 1)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConjunctionDesignated ( tableau / ** opts ) [source]
∧ ⊕
A ∧ B ⊕
⋮
¬A ⊖
A ⊖
¬B ⊖
B ⊖
From an unticked, designated conjunction node n on a branch b , add
four undesignated nodes to b , one for each conjunct, and one for the
negation of each conjunct. Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Conjunction), (Legend.designation, True))
The rule class legend.
name : str = 'ConjunctionDesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (30, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConjunctionNegatedDesignated ( tableau / ** opts ) [source]
From an unticked, designated, negated conjunction node n on a branch
b , make two branches b' and b'' from b . On b' add a designated
node with the first conjunct, and an undesignated node with the negation
of the second conjunct. On b'' add a designated node with the second
conjunct, and an undesignated node with the negation of the frist conjunct.
Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 1
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conjunction), (Legend.designation, True))
The rule class legend.
name : str = 'ConjunctionNegatedDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (30, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConjunctionUndesignated ( tableau / ** opts ) [source]
From an unticked, undesignated conjunction node n on a branch b , make
four branches b' , b'' , b''' , and b'''' from b . On b' , add a
designated node with the negation of the first conjunct. On b'' , add
a designated node ith the first conjunct. On b''' , add a designated
node with the negation of the second conjunct. On b'''' , add a designated
node with the second conjunct. Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 3
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Conjunction), (Legend.designation, False))
The rule class legend.
name : str = 'ConjunctionUndesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (30, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConjunctionNegatedUndesignated ( tableau / ** opts ) [source]
From an unticked, undesignated, negated conjunction node n on a branch
b , make three branches b' , b'' , and b''' from b . On b' , add
four undesignated nodes, one for each conjunct, and one for the negation
of each conjunct. On b'' , add a designated node with the negation of
the first conjunct. On b''' , add a designated node with the negation
of the second conjunct. Then tick n .
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 2
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conjunction), (Legend.designation, False))
The rule class legend.
name : str = 'ConjunctionNegatedUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (30, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialConditionalDesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.MaterialConditional), (Legend.designation, True))
The rule class legend.
name : str = 'MaterialConditionalDesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (50, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialConditionalNegatedDesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialConditional), (Legend.designation, True))
The rule class legend.
name : str = 'MaterialConditionalNegatedDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (50, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialConditionalUndesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.MaterialConditional), (Legend.designation, False))
The rule class legend.
name : str = 'MaterialConditionalUndesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (50, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialConditionalNegatedUndesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialConditional), (Legend.designation, False))
The rule class legend.
name : str = 'MaterialConditionalNegatedUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (50, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialBiconditionalDesignated ( tableau / ** opts ) [source]
≡ ⊕
A ≡ B ⊕
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊕
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.MaterialBiconditional), (Legend.designation, True))
The rule class legend.
name : str = 'MaterialBiconditionalDesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (60, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialBiconditionalNegatedDesignated ( tableau / ** opts ) [source]
¬ ≡ ⊕
¬(A ≡ B) ⊕
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊕
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialBiconditional), (Legend.designation, True))
The rule class legend.
name : str = 'MaterialBiconditionalNegatedDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (60, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialBiconditionalUndesignated ( tableau / ** opts ) [source]
≡ ⊖
A ≡ B ⊖
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊖
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.MaterialBiconditional), (Legend.designation, False))
The rule class legend.
name : str = 'MaterialBiconditionalUndesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (60, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class MaterialBiconditionalNegatedUndesignated ( tableau / ** opts ) [source]
¬ ≡ ⊖
¬(A ≡ B) ⊖
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊖
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialBiconditional), (Legend.designation, False))
The rule class legend.
name : str = 'MaterialBiconditionalNegatedUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (60, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConditionalDesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Conditional), (Legend.designation, True))
The rule class legend.
name : str = 'ConditionalDesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (70, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConditionalNegatedDesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conditional), (Legend.designation, True))
The rule class legend.
name : str = 'ConditionalNegatedDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (70, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConditionalUndesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Conditional), (Legend.designation, False))
The rule class legend.
name : str = 'ConditionalUndesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (70, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class ConditionalNegatedUndesignated ( tableau / ** opts ) [source]
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conditional), (Legend.designation, False))
The rule class legend.
name : str = 'ConditionalNegatedUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (70, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class BiconditionalDesignated ( tableau / ** opts ) [source]
↔ ⊕
A ↔ B ⊕
⋮
(A → B) ∧ (B → A) ⊕
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Biconditional), (Legend.designation, True))
The rule class legend.
name : str = 'BiconditionalDesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (80, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class BiconditionalNegatedDesignated ( tableau / ** opts ) [source]
¬ ↔ ⊕
¬(A ↔ B) ⊕
⋮
¬((A → B) ∧ (B → A)) ⊕
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = True
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Biconditional), (Legend.designation, True))
The rule class legend.
name : str = 'BiconditionalNegatedDesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (80, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class BiconditionalUndesignated ( tableau / ** opts ) [source]
↔ ⊖
A ↔ B ⊖
⋮
(A → B) ∧ (B → A) ⊖
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.operator, Operator.Biconditional), (Legend.designation, False))
The rule class legend.
name : str = 'BiconditionalUndesignated'
The rule class name.
negated : bool | None = None
operator : Operator | None = (80, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
class BiconditionalNegatedUndesignated ( tableau / ** opts ) [source]
¬ ↔ ⊖
¬(A ↔ B) ⊖
⋮
¬((A → B) ∧ (B → A)) ⊖
Parameters:
tableau (Tableau
Helpers : Mapping [ type [ Rule.Helper ] , Any ] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional(negated)>), ignore_ticked=True)})
Helper classes mapped to their settings.
NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}
branching : int = 0
The number of additional branches created.
defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
designation : bool | None = False
legend : tuple [ tuple [ str , Any ] , ... ] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Biconditional), (Legend.designation, False))
The rule class legend.
name : str = 'BiconditionalNegatedUndesignated'
The rule class name.
negated : bool | None = True
operator : Operator | None = (80, 2)
predicate : Predicate | None = None
quantifier : Quantifier | None = None
timer_names : Sequence [ str ] = qsetf({'search', 'apply'})
StopWatch names to create in timers
groups : tuple [ tuple [ type [ Rule ] , ... ] , ... ] = ((<class 'pytableaux.logics.fde.Rules.AssertionDesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionUndesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionNegatedUndesignated'>, <class 'pytableaux.logics.p3.Rules.ConjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionUndesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedDesignated'>, <class 'pytableaux.logics.p3.Rules.DoubleNegationDesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.p3.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.p3.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.p3.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.p3.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.p3.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.p3.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.p3.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.p3.Rules.BiconditionalNegatedDesignated'>, <class 'pytableaux.logics.p3.Rules.BiconditionalNegatedUndesignated'>), (<class 'pytableaux.logics.p3.Rules.DoubleNegationUndesignated'>, <class 'pytableaux.logics.p3.Rules.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedUndesignated'>), (<class 'pytableaux.logics.p3.Rules.ConjunctionNegatedUndesignated'>,), (<class 'pytableaux.logics.p3.Rules.ConjunctionUndesignated'>,))
