Information Model

# ModaLogic Functional/Technical Design Documentation

The Information Model Module¶

The Information Model Module provides abstractions for all the different types of modal logic expressions that the reasoner is able to process, interpret and reason about.

Of crucial importance in this case are the Formulas -- the abstractions of the various types of logical formulas -- that maintain the structure and content for these types of formulas. The following formulas (as defined by the logic systems that we support in the modalogic reasoner) are:

class Formula(object) : not actually called, but you may pretend that NegatedFormula etc. are all subclasses of Formula insofar as they inherit Formula.prototype.

class NegatedFormula(Formula) : this class represents a negated formula object that wraps around any other formula.

class BinaryFormula(Formula) : this class represents a formula object with an operand and has a left and right formula object e.g. A → B

class ModalFormula(Formula) : this class represents a modal formula object that has the '◇' or '□' functions in its expression.

class AtomicFormula(Formula) : this class repersents an atomic logic constant.

class QuantifiedFormula(Formula) : this class represents any fomula with the '∀' or '∃' symbol in it.

Each of these classes knows what its content (sub-functions) can be and it knows how to represent itself in an expression.

`formulas` ¶

`AtomicFormula` ¶

The atomic formula is either a logic constant or a logic function with a set of funcion terms.

Parameters:

Name	Type	Description	Default
`Formula`	`Formula`	base class	required

`substitute(self, origTerm, newTerm, shallow)` ¶

This function return new formula with all free occurrences of replaced by . If , don't replace terms in function arguments. This is particulary applied to the resolution of atomic formulas.

Parameters:

Name	Type	Description	Default
`origTerm`	`Formula`	the original logic formula	required
`newTerm`	`Formula`	the replacement logic formula	required
`shallow`	`bool`	whether or not to deep substitute or just in the original formula level.	required

Returns:

Type	Description
`Formula`	with replaced sub-formulas as requested.

Source code in modalogic\infomodel\formulas.py

def substitute(self, origTerm, newTerm, shallow):
    """This function return new formula with all free occurrences of <origTerm> replaced by <newTerm>. If <shallow>, don't replace terms in function arguments. This is particulary applied to the resolution of atomic formulas.

    Args:
        origTerm (Formula): the original logic formula
        newTerm (Formula): the replacement logic formula
        shallow (bool): whether or not to deep substitute or just in the original formula level.

    Returns:
        Formula: with replaced sub-formulas as requested.
    """
    if type(origTerm) == 'string' and self.string.indexOf(origTerm) == -1:
        return self

    newTerms = self.substituteInTerms(self.terms, origTerm, newTerm,
                                      shallow)
    if not self.terms.equals(newTerms):
        return AtomicFormula(self.predicate, newTerms)
    else:
        return self

`BinaryFormula` ¶

This class represents a formula object with an operand and a left and right formula object e.g. A → B

Parameters:

Name	Type	Description	Default
`Formula`	`Formula`	base class of the formula object.	required

`Formula` ¶

not actually called, but you may pretend that NegatedFormula etc. are all subclasses of Formula insofar as they inherit self.prototype.

Parameters:

Name	Type	Description	Default
`object`		None	required

Returns:

Type	Description
`Formula (Formula)`	base class for all logic formulas

`negate(self)` ¶

This function is used by a logic formula to wrap itself into a negated self.

Returns:

Type	Description
`NegatedFormula`	the self-formula now wrapped in a negated-formula

Source code in modalogic\infomodel\formulas.py

def negate(self):
    """This function is used by a logic formula to wrap itself into a negated self.

    Returns:
        NegatedFormula: the self-formula now wrapped in a negated-formula
    """
    return NegatedFormula(self)

`normalize(self)` ¶

This function returns an equivalent formula in negation normal form of the self self.

This is the standard rewriting that happens for implies functions and all the others. We basically want standard negation, 'and' 'or' logic functional rewrites.

Returns:

Type	Description
`Formula`	negation normal form of the self formula

Source code in modalogic\infomodel\formulas.py

def normalize(self):
    """This function returns an equivalent formula in negation normal form of the self self.

    This is the standard rewriting that happens for implies functions and all the others. We basically want standard negation, 'and' 'or' logic functional rewrites. 

    Returns:
       Formula: negation normal form of the self formula
    """
    if hasattr(self, "operator"):
        op = self.operator
    elif hasattr(self, "quantifier"):
        op = self.quantifier
    else:
        return self

    if op == '∧' or op == '∨':
        # |A&B| = |A|&|B|
        # |AvB| = |A|v|B|
        sub1 = self.sub1.normalize()
        sub2 = self.sub2.normalize()
        return BinaryFormula(op, sub1, sub2)

    elif op == '→':
        # |A->B| = |~A|v|B|
        sub1 = self.sub1.negate().normalize()
        sub2 = self.sub2.normalize()
        return BinaryFormula('∨', sub1, sub2)

    elif op == '↔':
        # |A<->B| = |A&B|v|~A&~B|
        sub1 = BinaryFormula('∧', self.sub1, self.sub2).normalize()
        sub2 = BinaryFormula('∧', self.sub1.negate(),
                             self.sub2.negate()).normalize()
        return BinaryFormula('∨', sub1, sub2)

    elif op == '∀' or op == '∃':
        # |(Ax)A| = Ax|A|
        nf = QuantifiedFormula(op,  self.variable, \
                                    self.matrix.normalize(), \
                                    self.overWorlds)
        return nf

    elif op == '□' or op == '◇':
        # |[]A| = []|A|
        return ModalFormula(op, self.sub.normalize())

    elif op == '¬':
        if hasattr(self.sub, "operator"):
            op2 = self.sub.operator
        elif hasattr(self.sub, "quantifier"):
            op2 = self.sub.quantifier
        else:
            return self

        if op2 == '∧' or op2 == '∨':
            # |~(A&B)| = |~A|v|~B|
            # |~(AvB)| = |~A|&|~B|
            sub1 = self.sub.sub1.negate().normalize()
            sub2 = self.sub.sub2.negate().normalize()
            newOp = '∨' if op2 == '∧' else '∧'
            return BinaryFormula(newOp, sub1, sub2)

        elif op2 == '→':
            # |~(A->B)| = |A|&|~B|
            sub1 = self.sub.sub1.normalize()
            sub2 = self.sub.sub2.negate().normalize()
            return BinaryFormula('∧', sub1, sub2)

        elif op2 == '↔':
            # |~(A<->B)| = |A&~B|v|~A&B|
            sub1 = BinaryFormula('∧', self.sub.sub1,
                                 self.sub.sub2.negate()).normalize()
            sub2 = BinaryFormula('∧', self.sub.sub1.negate(),
                                 self.sub.sub2).normalize()
            return BinaryFormula('∨', sub1, sub2)

        elif op2 == '∀' or op2 == '∃':
            # |~(Ax)A| = Ex|~A|
            # not( all x) == exists not x
            sub = self.sub.matrix.negate().normalize()
            return QuantifiedFormula('∃' if op2 == '∀' else '∀',
                                     self.sub.variable, sub,
                                     self.sub.overWorlds)

        elif op2 == '□' or op2 == '◇':
            # |~(□ A)| = ◇|~A|
            # |~(◇ A)| = □|~A|
            sub = self.sub.sub.negate().normalize()
            return ModalFormula('◇' if op2 == '□' else '□', sub)

        elif op2 == '¬':
            # |~~A| = |A|
            return self.sub.sub.normalize()

`ModalFormula` ¶

This class represents a formula object with amodal operator; diamond or box and a sub formula that is scopes.

Parameters:

Name	Type	Description	Default
`Formula`	`Formula`	base class of the formula object	required

`substitute(self, origTerm, newTerm, shallow)` ¶

This function returns a new formula with all free occurrences of replaced

by . If , don't replace terms in function arguments.¶

Parameters:

Name	Type	Description	Default
`origTerm`	`Formula`	the original logic formula	required
`newTerm`	`Formula`	the replacement logic formula	required
`shallow`	`bool`	whether or not to deep substitute or just in the original formula level.	required

Returns:

Type	Description
`Formula`	with replaced sub-formulas as requested.

Source code in modalogic\infomodel\formulas.py

def substitute(self, origTerm, newTerm, shallow):
    """This function returns a new formula with all free occurrences of <origTerm> replaced
    # by <newTerm>. If <shallow>, don't replace terms in function arguments.

    Args:
        origTerm (Formula): the original logic formula
        newTerm (Formula): the replacement logic formula
        shallow (bool): whether or not to deep substitute or just in the original formula level.

    Returns:
        Formula: with replaced sub-formulas as requested.
    """
    nsub = self.sub.substitute(origTerm, newTerm, shallow)
    if self.sub == nsub: return self
    return ModalFormula(self.operator, nsub)

`NegatedFormula` ¶

This class represents the negated form of a wrapped formula object.

Parameters:

Name	Type	Description	Default
`Formula`	`Formula`	base class of the formula object	required

`PredicateTermNode` ¶

The PredicateTermNode type maintains the information about a predicate formula that is represented in the form of a hierarchical data structure. It accepts UTF characters and is permissive of the function and constant predicate names. It is used in the "if is_atomic(comp_formula_s_)" function that parses the content of the propositional/predicate constants and predicate formulas.

!!! note "the nodetype is ∈ [:root, :constant, :variable, :predicate]. This is used during the unification process." The root means it is an irrelevant node to start the expression tree, The constant means it is an instantiated constant symbol, The variable means it is an uninstantiated variable symbol and The predicate means it is an predicate name symbol and a collection of parameters ∈

`QuantifiedFormula` ¶

This class represents a quantified formula with the existential or universal operator.

This class instance has a quantifier, a variable, a matrix/scope and an indicator for multi-world semantics worlds if needed.

Parameters:

Name	Type	Description	Default
`Formula`	`Formula`	base class	required

`substitute(self, origTerm, newTerm, shallow)` ¶

return new formula with all free occurrences of replaced by . If , don't replace terms in function arguments

Parameters:

Name	Type	Description	Default
`origTerm`	`[type]`	[description]	required
`newTerm`	`[type]`	[description]	required
`shallow`	`[type]`	[description]	required

Returns:

Type	Description
`QuantifiedFormula`	with all free occurrences of replaced by

Source code in modalogic\infomodel\formulas.py

def substitute(self, origTerm, newTerm, shallow):
    """ return new formula with all free occurrences of <origTerm> replaced by <newTerm>. If <shallow>, don't replace terms in function arguments

    Args:
        origTerm ([type]): [description]
        newTerm ([type]): [description]
        shallow ([type]): [description]

    Returns:
       QuantifiedFormula: with all free occurrences of <origTerm> replaced by <newTerm>
    """
    #
    if self.variable == origTerm: return self
    nmatrix = self.matrix.substitute(origTerm, newTerm, shallow)
    if nmatrix == self.matrix: return self
    return QuantifiedFormula(self.quantifier, self.variable, nmatrix,
                             self.overWorlds)

Last update: 2021-07-02

Information Model

The Information Model Module¶

formulas ¶

AtomicFormula ¶

substitute(self, origTerm, newTerm, shallow) ¶

BinaryFormula ¶

Formula ¶

negate(self) ¶

normalize(self) ¶

ModalFormula ¶

substitute(self, origTerm, newTerm, shallow) ¶

by . If , don't replace terms in function arguments.¶

NegatedFormula ¶

PredicateTermNode ¶

QuantifiedFormula ¶

substitute(self, origTerm, newTerm, shallow) ¶

`formulas` ¶

`AtomicFormula` ¶

`substitute(self, origTerm, newTerm, shallow)` ¶

`BinaryFormula` ¶

`Formula` ¶

`negate(self)` ¶

`normalize(self)` ¶

`ModalFormula` ¶

`substitute(self, origTerm, newTerm, shallow)` ¶

`NegatedFormula` ¶

`PredicateTermNode` ¶

`QuantifiedFormula` ¶

`substitute(self, origTerm, newTerm, shallow)` ¶