UniverseOfDiscourse (python class)
- class punctilious.UniverseOfDiscourse(symbol=None, dashed_name=None, name=None, echo=None)
This python class models a universe-of-discourse .
- property a: punctilious.core.AxiomDeclarationAccretor
The collection of axioms declared in this universe-of-discourse.
- Return type
AxiomDeclarationAccretor
- property c1: punctilious.core.ConnectiveAccretor
A python dictionary of connectives contained in this universe-of-discourse, where well-known connectives are directly available as properties.
- Return type
ConnectiveAccretor
- property c2: punctilious.core.ClassDeclarationAccretor
The collection of classes declared in this universe-of-discourse.
- Return type
ClassDeclarationAccretor
- property c3: punctilious.core.ConstantDeclarationDict
The collection of constants declared in this universe-of-discourse.
- Return type
ConstantDeclarationDict
- cross_reference_constant_OBSOLETE(c)
Cross-references a constant in this universe-of-discourse.
- Parameters
c (
ConstantDeclaration) – a constant-declaration.- Return type
bool
- property d: punctilious.core.DefinitionDeclarationAccretor
The collection of axioms declared in this universe-of-discourse.
- Return type
DefinitionDeclarationAccretor
- declare_compound_formula(connective, *terms, lock_variable_scope=None, symbol=None, index=None, auto_index=None, echo=None)
Declare a new formula in this universe-of-discourse.
This method is a shortcut for Formula(universe_of_discourse=self, . . d.).
A formula is declared in a theory, and not stated, because it is not a statement, i.e. it is not necessarily true in this theory.
- declare_theory(symbol=None, index=None, auto_index=None, dashed_name=None, name=None, explicit_name=None, ref=None, subtitle=None, extended_theory=None, extended_theory_limit=None, stabilized=False, echo=None)
Declare a new theory in this universe-of-discourse.
Shortcut for Theory(u, …).
- Parameters
nameset –
is_theory_foundation_system –
extended_theory –
- Returns
- declare_variable(symbol=None, dashed_name=None, acronym=None, abridged_name=None, name=None, explicit_name=None, is_strictly_propositional=None, echo=None)
Declare a variable in this universe-of-discourse.
A shortcut function for FreeVariable(universe_of_discourse=u, …)
- Parameters
symbol –
- Returns
- property i: punctilious.core.InferenceRuleDeclarationAccretor
The (possibly empty) collection of inference-rules declared in this in this universe-of-discourse .
Abridged name: i
- Return type
- property is_strictly_propositional: bool
Informs if a formula is propositional.
- Return type
bool- Returns
True if the formula is propositional, False otherwise.
- property metatheory: punctilious.core.PunctiliousMinimalMetatheory
A minimal metatheory for this universe-of-discourse.
- Return type
PunctiliousMinimalMetatheory
- property o: punctilious.core.SimpleObjctDict
The (possibly empty) collection of simple-objects declared in this in this universe-of-discourse.
Unabridged name: simple_objcts
Well-known simple-objcts are exposed as python properties. In general, a well-known simple-objct is declared in the universe-of-discourse the first time its property is accessed.
- Return type
SimpleObjctDict
- property simple_objcts: punctilious.core.SimpleObjctDict
The collection of simple-objcts in this universe-of-discourse.
Abridged version: u.o
Well-known simple-objcts are exposed as python properties. In general, a well-known simple-objct is declared in the universe-of-discourse the first time its property is accessed.
- Return type
SimpleObjctDict- Returns
- property symbolic_objects: punctilious.core.UniverseOfDiscourseSymbolicObjectAccretor
The collection of axioms declared in this universe-of-discourse.
- Return type
UniverseOfDiscourseSymbolicObjectAccretor
- property t: punctilious.core.TheoryDerivationDeclarationAccretor
The collection of theory-derivations declared in this universe-of-discourse.
- Return type
TheoryDerivationDeclarationAccretor
- take_note(t, content, symbol=None, index=None, auto_index=None, dashed_name=None, acronym=None, abridged_name=None, name=None, explicit_name=None, paragraph_header=None, ref=None, subtitle=None, echo=None)
Take a note, make a comment, or remark.
- with_variable(symbol=None, index=None, auto_index=None, dashed_name=None, acronym=None, abridged_name=None, name=None, explicit_name=None, echo=None)
Declare a variable in this universe-of-discourse.
This method is expected to be as in a with statement, it yields an instance of FreeVariable, and automatically lock the variable scope when the with left.
Example: with u.v(‘x’) as x, u.v(‘y’) as y: some code…
To manage variable scope extensions and locking expressly, use declare_variable() instead.