SEPLogic

Author

Marcel Simader

Date

13.07.2021

New in version 1.3.0.

SEPModules.maths.SEPLogic.Assignment

A type alias for a mapping of AtomicProposition objects to a bool truth value.

alias of Mapping[SEPModules.maths.SEPLogic.AtomicProposition, bool]

Exceptions

exception SEPModules.maths.SEPLogic.LogicError(msg, proposition)

LogicError is an exception class for errors in the SEPLogic module.

Parameters

  • msg (AnyStr) – the message of the error

  • proposition (AnyStr) – the string representation of the proposition which is related to the error

exception SEPModules.maths.SEPLogic.LogicSyntaxError(msg, proposition, file_path, lineno, offset, code_context)

LogicSyntaxError is an exception class for syntax errors in the SEPLogic module.

Parameters

  • msg (AnyStr) – the message of the error

  • proposition (AnyStr) – the string representation of the proposition which is related to the error

  • file_path (Union[AnyStr, os.PathLike]) – the path to the file where the error occurred

  • lineno (int) – the line number at which the error occurred in the file

  • offset (int) – the offset in characters for the syntax error ‘cursor’

  • code_context (List[AnyStr]) – the code context of where the error occurred (i.e. the source code)

static from_traceback(msg, proposition, tb, offset=0)

Creates a SEPSyntaxError object from a message, traceback, and an optional offset.

Parameters

  • msg (AnyStr) – the message of the error

  • proposition (AnyStr) – the string representation of the proposition which is related to the error

  • tb (inspect.Traceback) – the traceback to use as basis for the error

  • offset (int) – the offset in characters for the syntax error ‘cursor’

Returns

a new SEPSyntaxError instance

Return type

SEPModules.SEPUtils.SEPSyntaxError

Connective Bases

class SEPModules.maths.SEPLogic._Connective(value)

_Connective is the base class for connective enumerations. Each enumeration member must contain the method that this connective is associated with. It also stores an arity (see ConnectiveArity), and a “strength”.

The relational operators <, >, <=, >= of this instance compare the strength attribute, and the equivalency operators == and != compare strict object identity.

Parameters

  • method – the method corresponding to this connective

  • arity – the arity of this connective (see ConnectiveArity)

  • strength – an integer value defining this connective’s relative strength to the other connectives (for instance, negation is stronger than material implication)

property method: Callable
Returns

the method implementing the behavior of this connective

property arity: SEPModules.maths.SEPLogic.ConnectiveArity
Returns

the arity of this connective

property strength: int
Returns

the relative strength of this connective

final class SEPModules.maths.SEPLogic.ConnectiveArity(value)

ConnectiveArity is an enum representing the arity of a _Connective object. It contains an operand checking function which takes in the number of operands and returns whether this number is valid with the operator, and a description string.

The available members are as follows:

  • NILARY: exactly 0 operands (name is derived from word nil)

  • UNARY: exactly 1 operand

  • BINARY: exactly 2 operands

  • NARY: 2 or more operands (n-ary)

Param

a function which checks with the supplied number of operands whether the operator can be applied or not

Parameters

description – a short description of this arity for use in error and log output

property operand_check: Callable[[int], bool]
Returns

a function which checks if the supplied number of operands is valid

property description: str
Returns

a short description of this arity for use in log or error output

final class SEPModules.maths.SEPLogic.ConnectiveFormat(enumeration, entries)

ConnectiveFormat is a class which holds a mapping of _Connective objects to their respective ConnectiveFormat.Entry objects.

Parameters
class Entry(prefix, joiner, suffix)

ConnectiveFormat.Entry holds one entry of the mapping of ConnectiveFormat.

Parameters

  • prefix (str) – the string to prepend to the operands

  • joiner (str) – the string to use to join the operands (see str.join)

  • suffix (str) – the string o append to the operands

property prefix: str

The string to prepend to the operands.

property joiner: str

The string to use to join the operands (see str.join).

property suffix: str

The string to append to the operands.

property enumeration: Type[_ConnectiveEnum]

The _Connective enumeration this format defines.

format(*operands, connective)

Formats the operands with the given connective based on the format specified by the mapping in this class.

Parameters

  • operands (str) – an arbitrary number of operands as strings

  • connective (_ConnectiveEnum) – the connective from the specified enumeration enum class

Returns

the formatted string

Return type

str

Logical Connective Enum

final class SEPModules.maths.SEPLogic.LogicalConnective(value)

LogicalConnective is an enum deriving from _Connective. it contains the basic logical connectives:

  • EMPTY: no operator, empty (nilary)

  • NONE: no operator, identity (unary)

  • NEG: negation (unary)

  • EXIST: existential quantification (unary)

  • UNIV: universal quantification (unary)

  • AND: logical and (n-ary)

  • OR: logical or (n-ary)

  • R_IMPL: material “left-implies-right” implication (binary)

  • L_IMPL: material “right-implies-left” implication (binary)

  • IFF: material equivalence, biconditional “if-and-only-if” (binary)

class SEPModules.maths.SEPLogic.SupportsLogicalConnective(*args, **kwargs)

A simple protocol for indicating that the standard logical connective methods are supported by a class.

Connective Format Protocols

class SEPModules.maths.SEPLogic.SupportsConnectiveFormat(*args, **kwargs)

Protocol to check whether or not a class supports formatting by ConnectiveFormat.

class SEPModules.maths.SEPLogic.SupportsToPrettyPrint(*args, **kwargs)

Abstract base class for subclasses that can convert themselves to a pretty printed string.

to_pretty_print()

Converts this object to a pretty-printed string.

Returns

a pretty-printed string representation of this object

Return type

str

class SEPModules.maths.SEPLogic.SupportsToLimboole(*args, **kwargs)

Abstract base class for subclasses that can convert themselves to the limboole syntax as string.

to_limboole()

Converts this object to a limboole-compatible string.

Returns

a limboole-compatible string representation of this object

Return type

str

class SEPModules.maths.SEPLogic.SupportsToLaTeX(*args, **kwargs)

Abstract base class for subclasses that can convert themselves to LaTeX as string.

to_latex()

Converts this object to a LaTeX-compatible string.

Returns

a LaTeX-compatible string representation of this object

Return type

str

Proposition Protocols

class SEPModules.maths.SEPLogic.SupportsEval(*args, **kwargs)

Protocol to check whether or not an object can be evaluated using an assignment.

abstract eval(assignment)

Evaluates this object using assignment assignment and returns its truth value.

Parameters

assignment (Assignment) – the mapping (assignment) of truth values to AtomicProposition objects

Returns

the truth value of this object under assignment assignment

Return type

bool

class SEPModules.maths.SEPLogic.SupportsLimbooleEval(*args, **kwargs)

Abstract base class for an object that can be converted to limboole syntax and then evaluated by limboole.

limboole_eval(*option, timeout=1.0)

Passes the value generated by to_limboole() to the STDIN of a Python subprocess call to the program limboole with arguments option. Additionally, a timeout is specified to abort waiting for the program to return.

Parameters

  • option (str) – an arbitrary amount of strings which will be added to the called limboole command

  • timeout (Optional[float]) – a timeout in seconds after which the execution of the subprocess will be halted and a RuntimeError raised

Returns

the STDOUT of the program

Raises

LogicError – if there was an error while running the program, if the process timed out after the seconds specified by the timeout argument

Return type

str

Propositions

Proposition

class SEPModules.maths.SEPLogic.Proposition(*proposition, connective=None)

Proposition is the base class for representing a general propositional object. A general proposition consists of an arbitrary amount of composite Proposition objects connected by a _Connective. Upon creation of a proposition, the connective’s arity operand check function is called to ensure the correct number of composite propositions.

Aside from the propositions and connective, this class also keeps track of all of the seen connectives in its child proposition objects. It also keeps track of all the atomic propositions that have been seen in its child proposition objects (see AtomicProposition).

The class provides the following attributes for checking various characteristics of the structure of the proposition: empty, atomic, literal, quantifier, quantified.

The operations defined by LogicalConnective have been implemented in this class, which means that all propositions can be arbitrarily combined, with the mapping from operator to method being outlined in each member object of LogicalConnective. It is noteworthy to say that __mul__ (*) is mapped to __and__ (&), and __add__ (+) is mapped to __or__ (|) by default.

Note

All new instances of Proposition are normalized according to the static method normalize(), so that redundant constructions like nested LogicalConnective.NONE connectives can be avoided.

Warning

The boolean value of all Proposition objects is False by default and issues a syntax warning. If one desires to check the truth value of a proposition, the eval() method should be used with an assignment.

Parameters

  • proposition – an arbitrary number of Proposition objects

  • connective – a _Connective for defining the combining behavior of all passed propositions, usually a member of LogicalConnective, if None is given the constructor will try to use the correct connective when possible

Raises

ValueError – if no connective is given and the connective cannot be deduced from the other arguments, if the number of operands is incompatible with the given connective

static normalize(propositions, connective)

Normalizes the input to the initializer of a Proposition instance. The arguments to this function are the same arguments passed to __init__() but note that this function will not try to check or correct these inputs. The following rules are applied for \(a \in \mathcal{P}\), and \(P \in \mathcal{L}\):

\[\begin{split}\neg \top &{}\Rightarrow \bot \\ \neg \bot &{}\Rightarrow \top \\ \neg \neg a &{}\Rightarrow a \\ (a) &{}\Rightarrow a \\ P \land (a \land \cdots) &{}\Rightarrow P \land a \land \cdots \\ P \lor (a \lor \cdots) &{}\Rightarrow P \lor a \lor \cdots\end{split}\]

Note that in this notation, the parentheses \((\cdots)\) refer to a Proposition object which is nested within the unary LogicalConnective.NONE connective.

property propositions: Tuple[SEPModules.maths.SEPLogic.Proposition]
Returns

the child proposition instances of this class

property connective: SEPModules.maths.SEPLogic._Connective
Returns

the connective of this class, or LogicalConnective.NONE if no connective was defined

property seen_atomic_propositions: Set[SEPModules.maths.SEPLogic.AtomicProposition]

Gathers a set of all the atomic propositions that have been defined in any of the child proposition objects of this class.

Returns

a set of atomic propositions found in any of the child propositions of this class

property seen_connectives: Set[SEPModules.maths.SEPLogic._Connective]

Gathers a set of all the connectives that have been defined in any of the child proposition objects of this class.

Returns

a set of connectives found in any of the child propositions of this class

property empty: bool
Returns

whether or not this proposition contains child propositions

property atomic: bool
Returns

whether or not this proposition is atomic

property literal: bool
Returns

whether or not this proposition is a literal (i.e. atomic or a negation of an atomic proposition)

property quantifier: bool
Returns

whether or not this proposition is a quantifier (i.e. a literal proposition which is existentially or universally quantified)

property quantified: bool
Returns

whether or not this proposition contains any quantifiers (i.e. a proposition where any of the child propositions fulfill quantifier)

CNF()

Checks whether or not this formulas is in conjunctive normal form (counterpart to DNF()).

Returns

whether or not this formula is in CNF

Return type

bool

DNF()

Checks whether or not this formulas is in disjunctive normal form (counterpart to CNF()).

Returns

whether or not this formula is in DNF

Return type

bool

valid()

Checks whether or not this formula is valid using limboole.

Returns

whether or not this formula is valid

Raises

LogicError – if the proposition is quantified

Return type

bool

sat()

Checks whether or not this formula is satisfiable using limboole.

Returns

whether or not this formula is satisfiable

Raises

LogicError – if the proposition is quantified

Return type

bool

model()

Looks for a satisfying assignment (model) of this formula using limboole. If no such model is found and the formula is unsatisfiable, the empty dictionary is returned. The dictionary maps each AtomicProposition object of this class to a boolean truth value.

Returns

either a satisfying assignment as dictionary or the empty dictionary, if no such assignment exists

Raises

LogicError – if there was an error parsing the output model

Return type

Assignment

eval(assignment)

Evaluates this object using assignment assignment and returns its truth value.

Parameters

assignment (Assignment) – the mapping (assignment) of truth values to AtomicProposition objects

Returns

the truth value of this object under assignment assignment

Return type

bool

partial_eval(assignment, *, simplify=False)

Partially evaluate this proposition by replacing atomic propositions by the truth constants Top, or Bottom according to the given assignment.

See also

Proposition.eval()

Parameters

  • assignment (Assignment) – the (partial) assignment to apply to this proposition

  • simplify (bool) – whether or not to apply simplification rules to the proposition after applying the assignment

Returns

the partially evaluated proposition

Raises

LogicError – if the proposition is quantified

Return type

SEPModules.maths.SEPLogic.Proposition

simplify_neg()

Perform simplification steps regarding the negations in this proposition. The following rules are applied for \(a, b \in \mathcal{P}\), and a proposition \(P \in \mathcal{L}\):

\[\begin{split}\neg \neg a &{}\Longrightarrow a \\ \neg (a \rightarrow b) &{}\Longrightarrow a \lor \neg b \\ \neg (a \leftarrow b) &{}\Longrightarrow \neg a \lor b \\ \neg (a \leftrightarrow b) &{}\Longrightarrow (a \lor b) \land (\neg a \lor \neg b) \\ \neg \exists a : P &{}\Longrightarrow \forall a : \neg P \\ \neg \forall a : P &{}\Longrightarrow \exists a : \neg P \\ \neg (a \land b \land \cdots) &{}\Longrightarrow \neg a \lor \neg b \lor \cdots \\ \neg (a \lor b \lor \cdots) &{}\Longrightarrow \neg a \land \neg b \land \cdots\end{split}\]
Returns

the simplified proposition

Return type

SEPModules.maths.SEPLogic.Proposition

reduce()

Reduce this proposition, so that its syntactic representation is more compact. The following rules are applied for \(a, b \in \mathcal{P}\), and propositions \(P, Q, R, S \in \mathcal{L}\):

\[a \leftarrow b :\Longleftrightarrow b \rightarrow a\]
\[\begin{split}\bot \rightarrow a &{}\Longrightarrow \top \\ a \rightarrow \top &{}\Longrightarrow \top \\ a \rightarrow a &{}\Longrightarrow \top \\ a \land b \land \cdots \rightarrow a &{}\Longrightarrow \top \\ a \rightarrow a \lor b \lor \dots &{}\Longrightarrow \top \\ a \rightarrow \bot &{}\Longrightarrow \neg a \\ \top \rightarrow a &{}\Longrightarrow a \\ a \rightarrow \neg a \land b \land \cdots &{}\Longrightarrow \neg a \\ \neg a \rightarrow a \land b \land \cdots &{}\Longrightarrow a \\ a \lor b \lor \cdots \rightarrow \neg a &{}\Longrightarrow \neg a \\ \neg a \lor b \lor \cdots \rightarrow a &{}\Longrightarrow a\end{split}\]
\[\begin{split}a \leftrightarrow \top &{}\Longrightarrow a \\ \top \leftrightarrow a &{}\Longrightarrow a \\ a \leftrightarrow \bot &{}\Longrightarrow \neg a \\ \bot \leftrightarrow a &{}\Longrightarrow \neg a \\ a \leftrightarrow a &{}\Longrightarrow \top \\ \neg a \leftrightarrow a &{}\Longrightarrow \bot \\ a \leftrightarrow \neg a &{}\Longrightarrow \bot\end{split}\]
\[\begin{split}\top \land P &{}\Longrightarrow P \\ \bot \land \cdots &{}\Longrightarrow \bot \\ \top \lor \cdots &{}\Longrightarrow \top \\ \bot \lor P &{}\Longrightarrow P \\ a \lor \neg a \lor \cdots &{}\Longrightarrow \top \\ a \land \neg a \land \cdots &{}\Longrightarrow \bot \\ a \land (a \lor \cdots) \land P &{}\Longrightarrow a \land P \\ a \lor (a \land \cdots) \lor P &{}\Longrightarrow a \lor P \\ (P \land Q) \lor (P \land R) \lor S &{}\Longrightarrow \big(P \land (Q \lor R)\big) \lor S \\ (P \lor Q) \land (P \lor R) \land S &{}\Longrightarrow \big(P \lor (Q \land R)\big) \land S \\ \neg P \lor Q \lor R &{}\Longrightarrow (P \rightarrow Q) \lor R \\ P \lor \neg Q \lor R &{}\Longrightarrow (Q \rightarrow P) \lor R \\ (P \rightarrow Q) \land (Q \rightarrow P) \land R &{}\Longrightarrow (P \leftrightarrow Q) \land R\end{split}\]
Returns

the reduced proposition

Return type

SEPModules.maths.SEPLogic.Proposition

expand()

Expand this proposition, so that its syntactic representation is less compact. The following rules are applied for \(a, b, c \in \mathcal{P}\), and a proposition \(P \in \mathcal{L}\):

\[\begin{split}a \rightarrow b &{}\Longrightarrow \neg a \lor b \\ a \leftarrow b &{}\Longrightarrow a \lor \neg b \\ a \leftrightarrow b &{}\Longrightarrow (a \land b) \lor (\neg a \land \neg b) \\ a \land (b \lor c \lor \cdots) \land P &{}\Longrightarrow \big((a \land b) \lor (a \land c) \lor \cdots\big) \land P \\ a \lor (b \land c \land \cdots) \lor P &{}\Longrightarrow \big((a \lor b) \land (a \lor c) \land \cdots\big) \lor P\end{split}\]
Returns

the expanded proposition

Return type

SEPModules.maths.SEPLogic.Proposition

copy()

Copies this proposition into a new proposition object. This is a deep copy of all containing propositions.

Returns

a deep copy of this proposition object

Return type

SEPModules.maths.SEPLogic.Proposition

syntactically_equal(other)

Compare two propositions syntactically based on their computed hash.

Parameters

other – the proposition to compare against

Returns

whether or not cls is syntactically equivalent to other

Return type

bool

Atomic Proposition

class SEPModules.maths.SEPLogic.AtomicProposition

AtomicProposition represents the smallest unit of a Proposition, aside from the empty formula. Each new instance of AtomicProposition is uniquely assigned an id defined by the system’s current time in nanoseconds and a random __offset. The class registers this id in a set to avoid the slim chance of a duplicate. All subclasses should, if they desire a custom implementation of the id system, register it like so: AtomicProposition._id_set.add(id).

Each AtomicProposition object, besides the id, also has a unique volatile_name. As the name suggests, this name does not guarantee to be unique over multiple runtimes and is subject to change at any point. It is used when generating the to_limboole() and __str__() format outputs. The naming convention is given as regular expression ^[a-z](')*$ for pretty-printed, and ^[a-z](-prime)*$ for limboole output.

This class, as well as each class subclassing AtomicProposition will contain the class attributes defining how the volatile_name of an object should behave. Each new subclass will start the name back at the lowest character at the lowest “prime characters” count. To keep names unique, each name will be prefixed with the subclass’ name. This behaviour may be changed but with caution.

To get the next volatile name for a new object, use the class method _next_volatile_name(). To get the next id for a new object, use the static method _next_id().

The exception are the special Top and Bottom singleton objects. Top will always be assigned id 1 and volatile name top, and Bottom will always be assigned id 0 and volatile name bottom. The pretty-printed outputs of top and bottom are the down-tick and up-tick symbols respectively, and the limboole outputs are (top | !top) and (bottom & !bottom) since limboole does not support these truth values natively.

static normalize(propositions, connective)

Normalizes the input to the initializer of a Proposition instance. The arguments to this function are the same arguments passed to __init__() but note that this function will not try to check or correct these inputs. The following rules are applied for \(a \in \mathcal{P}\), and \(P \in \mathcal{L}\):

\[\begin{split}\neg \top &{}\Rightarrow \bot \\ \neg \bot &{}\Rightarrow \top \\ \neg \neg a &{}\Rightarrow a \\ (a) &{}\Rightarrow a \\ P \land (a \land \cdots) &{}\Rightarrow P \land a \land \cdots \\ P \lor (a \lor \cdots) &{}\Rightarrow P \lor a \lor \cdots\end{split}\]

Note that in this notation, the parentheses \((\cdots)\) refer to a Proposition object which is nested within the unary LogicalConnective.NONE connective.

final static _next_id(requested_id=None)

Get the next available id. If requested_id is passed, then that id will be returned if it is valid and has not been used by another object.

Parameters

requested_id (Optional[int]) – optional, the requested id

Returns

the requested id or the next valid id if no requested id was passed or if the requested id was taken already

Return type

int

classmethod _next_volatile_name()

Get the next available volatile name.

Returns

the next volatile name as string

Return type

str

property id: int
Returns

the id of this atomic proposition object

property volatile_name: str
Returns

the volatile name of this atomic proposition object

eval(assignment)

Evaluates this object using assignment assignment and returns its truth value.

Parameters

assignment (Assignment) – the mapping (assignment) of truth values to AtomicProposition objects

Returns

the truth value of this object under assignment assignment

Return type

bool

copy()

Copies this proposition into a new proposition object. This is a deep copy of all containing propositions.

Returns

a deep copy of this proposition object

Return type

SEPModules.maths.SEPLogic.AtomicProposition

Truth constants

SEPModules.maths.SEPLogic.Top: Final[_Top] = Top

The singleton object representing the truth value True.

SEPModules.maths.SEPLogic.Bottom: Final[_Bottom] = Bottom

The singleton object representing the truth value False.