diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 56270a85d..ea0a241da 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -7,7 +7,8 @@
-
+
+
@@ -120,7 +121,7 @@
-
+
@@ -228,7 +229,7 @@
-
+
@@ -240,7 +241,7 @@
-
+
@@ -249,7 +250,7 @@
-
+
@@ -261,7 +262,7 @@
-
+
@@ -331,7 +332,7 @@
-
+
@@ -341,11 +342,11 @@
-
+
-
+
@@ -355,11 +356,11 @@
-
+
-
+
@@ -369,7 +370,7 @@
-
+
@@ -394,23 +395,23 @@
+
@@ -423,22 +424,6 @@
1687980987309
-
-
- 1694728065674
-
-
-
- 1694728065674
-
-
-
- 1694728082557
-
-
-
- 1694728082557
-
1694777914447
@@ -815,7 +800,23 @@
1696020173067
-
+
+
+ 1696109485247
+
+
+
+ 1696109485247
+
+
+
+ 1696109556899
+
+
+
+ 1696109556899
+
+
diff --git a/src/punctilious/core.py b/src/punctilious/core.py
index 5f5403bf3..88a00f0e3 100644
--- a/src/punctilious/core.py
+++ b/src/punctilious/core.py
@@ -2603,14 +2603,28 @@ def __init__(self, relation: (Relation, FreeVariable), parameters: tuple,
nameset = NameSet(symbol=symbol, index=index)
self.relation = relation
parameters = parameters if isinstance(parameters, tuple) else tuple([parameters])
+ verify(assertion=len(parameters) > 0,
+ msg='Ill-formed formula error. The number of parameters in this formula is zero. 0-ary relations are currently not supported. Use a simple-object instead.',
+ severity=verification_severities.error, raise_exception=True, relation=self.relation,
+ len_parameters=len(parameters))
+ verify(assertion=self.relation.arity is None or self.relation.arity == len(parameters),
+ msg=f'Ill-formed formula error. Relation ⌜{self.relation}⌝ is defined with a fixed arity constraint of {self.relation.arity} but the number of parameters provided to construct this formula is {len(parameters)}.',
+ severity=verification_severities.error, raise_exception=True, relation=self.relation,
+ relation_arity=self.relation.arity, len_parameters=len(parameters),
+ parameters=parameters)
+ verify(
+ assertion=self.relation.min_arity is None or self.relation.min_arity >= len(parameters),
+ msg=f'Ill-formed formula error. Relation ⌜{self.relation}⌝ is defined with a minimum arity constraint of {self.relation.min_arity} but the number of parameters provided to construct this formula is {len(parameters)}.',
+ severity=verification_severities.error, raise_exception=True, relation=self.relation,
+ relation_min_arity=self.relation.min_arity, len_parameters=len(parameters),
+ parameters=parameters)
+ verify(
+ assertion=self.relation.max_arity is None or self.relation.max_arity >= len(parameters),
+ msg=f'Ill-formed formula error. Relation ⌜{self.relation}⌝ is defined with a maximum arity constraint of {self.relation.max_arity} but the number of parameters provided to construct this formula is {len(parameters)}.',
+ severity=verification_severities.error, raise_exception=True, relation=self.relation,
+ relation_max_arity=self.relation.max_arity, len_parameters=len(parameters),
+ parameters=parameters)
self.arity = len(parameters)
- verify(self.arity > 0,
- 'The number of parameters in this formula is zero. 0-ary relations are currently not '
- 'supported.')
-
- verify(is_in_class(relation, classes.free_variable) or self.relation.arity == self.arity,
- 'The arity of this formula''s relation is inconsistent with the number of parameters '
- 'in the formula.', relation=self.relation, parameters=parameters)
self.parameters = parameters
super().__init__(nameset=nameset, universe_of_discourse=universe_of_discourse, echo=False)
super()._declare_class_membership(declarative_class_list.formula)
@@ -3919,20 +3933,26 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
name = 'biconditional elimination #2'
with u.v(symbol='P') as p, u.v(symbol='Q') as q:
definition = ((p | u.r.iff | q) | u.r.proves | (q | u.r.implies | p))
+ with u.v(symbol='P') as p, u.v(symbol='Q') as q:
+ self.parameter_p_iff_q = p | u.r.iff | q
+ self.parameter_p_iff_q_mask = frozenset([p, q])
super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
- def infer_formula(self, p_iff_q: FormulaStatement = None, t: TheoryElaborationSequence = None,
- echo: (None, bool) = None) -> Formula:
+ def construct_formula(self, p_iff_q: FormulaStatement = None) -> Formula:
"""
.. include:: ../../include/construct_formula_python_method.rstinc
"""
- p_iff_q: Formula = verify_formula(u=self.u, arity=2, input_value=p_iff_q)
- p: Formula = verify_formula(u=self.u, arity=None, input_value=p_iff_q.parameters[0])
- q: Formula = verify_formula(u=self.u, arity=None, input_value=p_iff_q.parameters[1])
- output = (q | t.u.r.implies | p)
+ ok: bool
+ msg: (None, msg)
+ ok, p_iff_q, msg = verify_formula(arg='p_iff_q', input_value=p_iff_q, u=self.u,
+ form=self.parameter_p_iff_q, mask=self.parameter_p_iff_q_mask, raise_exception=True)
+ p_iff_q: Formula
+ p: Formula = p_iff_q.parameters[0]
+ q: Formula = p_iff_q.parameters[1]
+ output = (q | self.u.r.implies | p)
return output
@@ -3958,21 +3978,39 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
with u.v(symbol='P') as p, u.v(symbol='Q') as q:
definition = (((p | u.r.implies | q) | u.r.sequent_comma | (
q | u.r.implies | p)) | u.r.proves | (p | u.r.iff | q))
+ with u.v(symbol='P') as p, u.v(symbol='Q') as q:
+ self.parameter_p_implies_q = p | u.r.implies | q
+ self.parameter_p_implies_q_mask = frozenset([p, q])
+ with u.v(symbol='P') as p, u.v(symbol='Q') as q:
+ self.parameter_q_implies_p = q | u.r.iff | p
+ self.parameter_q_implies_p_mask = frozenset([p, q])
super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
- def infer_formula(self, p_implies_q: (tuple, Formula, FormulaStatement) = None,
- q_implies_p: (tuple, Formula, FormulaStatement) = None,
- t: TheoryElaborationSequence = None, echo: (None, bool) = None) -> Formula:
+ def construct_formula(self, p_iff_q: FormulaStatement = None) -> Formula:
"""
.. include:: ../../include/construct_formula_python_method.rstinc
"""
- p_implies_q = verify_formula(u=t.u, arity=2, input_value=p_implies_q)
- p = p_implies_q.parameters[0]
- q = p_implies_q.parameters[1]
- return p | t.u.r.iff | q
+ ok: bool
+ msg: (None, msg)
+ ok, p_implies_q, msg = verify_formula(arg='p_implies_q', input_value=p_implies_q, u=self.u,
+ form=self.parameter_p_implies_q, mask=self.parameter_p_implies_q_mask,
+ raise_exception=True)
+ p_implies_q: Formula
+ ok, q_implies_p, msg = verify_formula(arg='q_implies_p', input_value=q_implies_p, u=self.u,
+ form=self.parameter_q_implies_p, mask=self.parameter_q_implies_p_mask,
+ raise_exception=True)
+ q_implies_p: Formula
+ p_implies_q__p: Formula = p_implies_q.parameters[0]
+ # TODO: Do not is but use is_syntactically_equivalent instead.
+ verify(assertion=p_implies_q.parameters[0] is p_implies_q.parameters[1], msg='The ⌜p⌝ in ',
+ severity=verification_severities.error, raise_exception=True)
+ p: Formula = p_implies_q.parameters[0]
+ q: Formula = p_implies_q.parameters[1]
+ output = (q | self.u.r.implies | p)
+ return output
class ConjunctionElimination1Declaration(InferenceRuleDeclaration):
@@ -5577,7 +5615,8 @@ class Relation(TheoreticalObject):
"""The Relation pythonic class is the implementation of the relation theoretical-object.
"""
- def __init__(self, universe_of_discourse: UniverseOfDiscourse, arity: int,
+ def __init__(self, universe_of_discourse: UniverseOfDiscourse, arity: (None, int) = None,
+ min_arity: (None, int) = None, max_arity: (None, int) = None,
symbol: (None, str, StyledText) = None, index: (None, int) = None,
auto_index: (None, bool) = None, formula_rep=None, signal_proposition=None,
signal_theoretical_morphism=None, implementation=None,
@@ -5586,6 +5625,29 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, arity: int,
explicit_name: (None, str, StyledText) = None, ref: (None, str, StyledText) = None,
subtitle: (None, str, StyledText) = None, nameset: (None, str, NameSet) = None,
echo: (None, bool) = None):
+ """
+
+ :param universe_of_discourse:
+ :param arity: A fixed arity constraint for well-formed formula. Formulae based on this relation with distinct arity are ill-formed. Equivalent to passing the same value to both min_arity, and max_arity.
+ :param min_arity: A fixed minimum (inclusive) arity constraint for well-formed formula. Formulae based on this relation with lesser arity are ill-formed.
+ :param max_arity: A fixed maximum (inclusive) arity constraint for well-formed formula. Formulae based on this relation with greater arity are ill-formed.
+ :param symbol:
+ :param index:
+ :param auto_index:
+ :param formula_rep:
+ :param signal_proposition:
+ :param signal_theoretical_morphism:
+ :param implementation:
+ :param dashed_name:
+ :param acronym:
+ :param abridged_name:
+ :param name:
+ :param explicit_name:
+ :param ref:
+ :param subtitle:
+ :param nameset:
+ :param echo:
+ """
echo = prioritize_value(echo, configuration.echo_relation, configuration.echo_default,
False)
auto_index = prioritize_value(auto_index, configuration.auto_index, True)
@@ -5599,8 +5661,9 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, arity: int,
self.signal_proposition = signal_proposition
self.signal_theoretical_morphism = signal_theoretical_morphism
self.implementation = implementation
- assert arity is not None and isinstance(arity, int) and arity > 0
self.arity = arity
+ self.min_arity = min_arity
+ self.max_arity = max_arity
if nameset is None:
symbol = configuration.default_relation_symbol if symbol is None else symbol
index = universe_of_discourse.index_symbol(symbol=symbol) if auto_index else index
@@ -6774,17 +6837,18 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
proof=proof)
- def check_inference_validity(self, p_iff_q: FormulaStatement = None,
- t: TheoryElaborationSequence = None) -> bool:
- p_iff_q: FormulaStatement = verify_formula_statement(t=t, arity=None, input_value=p_iff_q)
- verify(t.contains_theoretical_objct(p_iff_q),
- 'Formula-statement ⌜p_iff_q⌝ must be contained in theory ⌜t⌝.', phi=p_iff_q, t=t,
- slf=self)
- p_iff_q: Formula = verify_formula(u=self.u, arity=None, input_value=p_iff_q)
- verify(p_iff_q.relation is t.u.r.biconditional,
- 'The relation of formula ⌜p_iff_q⌝ must be a biconditional.',
- phi_relation=p_iff_q.relation, phi=p_iff_q, t=t, slf=self)
- return True
+ def check_premises_validity(self, p_iff_q: FlexibleFormula,
+ raise_exception: bool = True) -> bool:
+ """
+ .. include:: ../../include/check_premises_validity_python_method.rstinc
+
+ """
+ # Validate that expected formula-statements are formula-statements.
+ formula_ok, _, _ = verify_formula_statement(t=self.t, input_value=p_iff_q,
+ form=self.i.parameter_p_iff_q, mask=self.i.parameter_p_iff_q_mask,
+ raise_exception=raise_exception)
+ # The method either raises an exception during validation, or return True.
+ return formula_ok
def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
Composable, Composable, bool]:
@@ -6792,22 +6856,29 @@ def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Gener
o=o)
return output
- def infer_formula(self, p_iff_q: (None, FormulaStatement) = None, echo: (None, bool) = None):
+ @property
+ def i(self) -> BiconditionalElimination1Declaration:
+ """Override the base class i property with a specialized inherited class type."""
+ i: BiconditionalElimination1Declaration = super().i
+ return i
+
+ def construct_formula(self, p_iff_q: FlexibleFormula) -> Formula:
"""
.. include:: ../../include/construct_formula_python_method.rstinc
"""
- return super().infer_formula(p_iff_q, echo=echo)
+ # Call back the infer_formula method on the inference-rule declaration class.
+ return self.i.construct_formula(p_iff_q=p_iff_q)
- def infer_formula_statement(self, p_iff_q: (None, FormulaStatement) = None,
- nameset: (None, str, NameSet) = None, ref: (None, str) = None,
+ def infer_formula_statement(self, p_iff_q: FlexibleFormula = None, ref: (None, str) = None,
paragraph_header: (None, ParagraphHeader) = None, subtitle: (None, str) = None,
echo: (None, bool) = None) -> InferredStatement:
"""
.. include:: ../../include/infer_formula_statement_python_method.rstinc
"""
- return super().infer_formula_statement(p_iff_q, nameset=nameset, ref=ref,
+ premises = self.i.Premises(p_iff_q=p_iff_q)
+ return InferredStatement(i=self, premises=premises, ref=ref,
paragraph_header=paragraph_header, subtitle=subtitle, echo=echo)
diff --git a/src/sample/sample_biconditional_elimination_2.py b/src/sample/sample_biconditional_elimination_2.py
index 81112214f..f1290e14d 100644
--- a/src/sample/sample_biconditional_elimination_2.py
+++ b/src/sample/sample_biconditional_elimination_2.py
@@ -13,7 +13,7 @@
t1 = u.t(echo=True)
theory_axiom = t1.include_axiom(a=axiom)
phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
- formula=r1(o1, o2) | u.r.biconditional | r2(o3))
+ p=r1(o1, o2) | u.r.biconditional | r2(o3))
# And finally, use the biconditional-elimination-2 inference-rule:
proposition_of_interest = t1.i.biconditional_elimination_2.infer_formula_statement(p_iff_q=phi1,
diff --git a/tests/test_formula.py b/tests/test_formula.py
index 4a0d8c92c..7511df1ff 100644
--- a/tests/test_formula.py
+++ b/tests/test_formula.py
@@ -15,28 +15,32 @@ def test_formula(self):
r3 = u.r.declare(arity=1, formula_rep=pu.Formula.postfix)
r4 = u.r.declare(arity=2, formula_rep=pu.Formula.function_call)
r5 = u.r.declare(arity=2, formula_rep=pu.Formula.infix)
+ r6 = u.r.declare(arity=3, formula_rep=pu.Formula.function_call)
phi1 = u.f(r1, o1)
phi2 = u.f(r2, o1)
phi3 = u.f(r3, o1)
phi4 = u.f(r4, o1, o2)
phi5 = u.f(r5, o1, o2)
+ phi6 = u.f(r6, o1, o2, o1)
self.assertEqual('r1(o1)', str(phi1.rep_formula(encoding=pu.encodings.plaintext)))
self.assertEqual('𝑟₁(𝑜₁)', str(phi1.rep_formula(encoding=pu.encodings.unicode)))
self.assertEqual('\\mathit{r}_{1}\\left(\\mathit{o}_{1}\\right)',
- str(phi1.rep_formula(encoding=pu.encodings.latex)))
+ str(phi1.rep_formula(encoding=pu.encodings.latex)))
self.assertEqual('r2(o1)', str(phi2.rep_formula(encoding=pu.encodings.plaintext)))
self.assertEqual('𝑟₂(𝑜₁)', str(phi2.rep_formula(encoding=pu.encodings.unicode)))
self.assertEqual('\\mathit{r}_{2}\\left(\\mathit{o}_{1}\\right)',
- str(phi2.rep_formula(encoding=pu.encodings.latex)))
+ str(phi2.rep_formula(encoding=pu.encodings.latex)))
self.assertEqual('(o1)r3', str(phi3.rep_formula(encoding=pu.encodings.plaintext)))
self.assertEqual('(𝑜₁)𝑟₃', str(phi3.rep_formula(encoding=pu.encodings.unicode)))
self.assertEqual('\\left(\\mathit{o}_{1}\\right)\\mathit{r}_{3}',
- str(phi3.rep_formula(encoding=pu.encodings.latex)))
+ str(phi3.rep_formula(encoding=pu.encodings.latex)))
self.assertEqual('r4(o1, o2)', str(phi4.rep_formula(encoding=pu.encodings.plaintext)))
self.assertEqual('𝑟₄(𝑜₁, 𝑜₂)', str(phi4.rep_formula(encoding=pu.encodings.unicode)))
self.assertEqual('\\mathit{r}_{4}\\left(\\mathit{o}_{1}, \\mathit{o}_{2}\\right)',
- str(phi4.rep_formula(encoding=pu.encodings.latex)))
+ str(phi4.rep_formula(encoding=pu.encodings.latex)))
self.assertEqual('(o1 r5 o2)', str(phi5.rep_formula(encoding=pu.encodings.plaintext)))
self.assertEqual('(𝑜₁ 𝑟₅ 𝑜₂)', str(phi5.rep_formula(encoding=pu.encodings.unicode)))
self.assertEqual('\\left(\\mathit{o}_{1} \\mathit{r}_{5} \\mathit{o}_{2}\\right)',
- str(phi5.rep_formula(encoding=pu.encodings.latex)))
+ str(phi5.rep_formula(encoding=pu.encodings.latex)))
+ self.assertEqual('r6(o1, o2, o1)', str(phi6.rep_formula(encoding=pu.encodings.plaintext)))
+ self.assertEqual('𝑟₆(𝑜₁, 𝑜₂, 𝑜₁)', str(phi6.rep_formula(encoding=pu.encodings.unicode)))