ModaLogic Architecture Documentation¶

The Parser Feature¶

`argumentparser` ¶

`ArgumentParser` ¶

The ArgumentParser type maintains the state of the parsing process at the level of the argument. An argument is either a set of premises and a concusion on just a conclusion statement. Each of these is a formula that is processed in turn by the FormulaParser. The collection of resulting formula objects forms the basis for the semantic tableaux evaluation. The FormulaParser returns the formula object for each of the premises and conclusion strings.

`prepare_formula(self, prep_formula, from_ascii=True)` ¶

This function will remove all the white space from the input string and it replaces all brackets types with parenthesis and remove parens from the around the quantifiers: (∀x)F(x) => ∀xF(x). It optionally will do a symbol replacement on the string first if it is written in ascii text.

Parameters:

Name	Type	Description	Default
`prep_formula`	`str`	the formula expression to clean up	required
`from_ascii`	`bool`	indicates an ascii expression to convert. Defaults to True.	`True`

Returns:

Type	Description
`str`	str:cleaned up expression string for the whole argument.

Source code in modalogic\parser\argumentparser.py

def prepare_formula(self, prep_formula:str, from_ascii:bool=True) -> str:
    """This function will remove all the white space from the input string and it replaces all brackets types with parenthesis and remove parens from the around the quantifiers: (∀x)F(x) => ∀xF(x). It optionally will do a symbol replacement on the string first if it is written in ascii text.

    Args:
        prep_formula (str): the formula expression to clean up
        from_ascii (bool, optional): indicates an ascii expression to convert. Defaults to True.

    Returns:
        str:cleaned up expression string for the whole argument.
    """
    # 1. convert all asii representations to UTF symbols
    # 2: remove all whitespace
    # 3: replace all ']['with ')('
    # 4: remove parentheses around quantifiers: (∀x)Fx => ∀xFx

    cf = prep_formula
    if from_ascii:
        cf = ExpressionRewriter.toSymbols(cf)
    cf = re.sub(r"\s+", r"",cf)
    cf = re.sub(r"\[", r"(",cf)
    cf = re.sub(r"\]", r")",cf)
    cf = re.sub(r"\(([∀∃]\w\d*)\)", r"\1",cf)
    self.argument_s = cf
    return self.argument_s

`process_argument(self)` ¶

This function takes the prepared argument string and asserts that it is a correct argument syntax after which it separates out each of the premises and the conclusion(s) --the premises are split from the conclusion by the turnstile symbol-- into separate strings that will each be parsed into a Formula object. The premises end up in a list and the conclusion as a property of itself.

Source code in modalogic\parser\argumentparser.py

def process_argument(self):
    """This function takes the prepared argument string and asserts that it is a correct argument syntax after which it separates out each of the premises and the conclusion(s) --the premises are split from the conclusion by the turnstile symbol-- into separate strings that will each be parsed into a Formula object. The premises end up in a list and the conclusion as a property of itself.
    """
    assert 1 == self.argument_s.count('⊧')
    leftparencount = self.argument_s.count(')')
    rightparencount =  self.argument_s.count(')')
    assert(leftparencount==rightparencount)

    premises = []

    self.argument_s = self.prepare_formula(self.argument_s)
    premises_s,conclusion_s = self.argument_s.split('⊧')
    self.conclusion_s = conclusion_s

    if premises_s:
        premises_ss = premises_s.split(';')
        self.premises_ss = premises_ss
        for p_s in premises_ss:
            fparser = FormulaParser()
            fparser.symboltable = self.symboltable
            formula = fparser.process_formula(p_s)
            premises.append(formula)
        self.premises = premises

    if conclusion_s != "":
        fparser = FormulaParser()
        fparser.symboltable = self.symboltable
        formula = fparser.process_formula(conclusion_s)
        self.conclusion = formula
    pass

`formulaparser` ¶

`FormulaParser` ¶

The FormulaParser maintains the state of the parsing process at the level of a single formula in an argument. If there are no premises we only call the FormulaParser on the conclusion but we need to maintain a symbol table across all premises and the conclusion so this is handled by the ArgumentParser (see modalogic.parsers.argumentparser)

`extract_atomic(self, atomic_s_)` ¶

1	`extract_atomic(atomic_s_:AbstractString)`

This function either returns an atomic proposition constant or a predicate formula constant.

Source code in modalogic\parser\formulaparser.py

def extract_atomic(self, atomic_s_:str):
    """
        extract_atomic(atomic_s_:AbstractString)

    This function either returns an atomic proposition constant or a predicate formula constant.
    """
    atomic = self.extract_atomicprop(atomic_s_)
    atomic = (atomic, 'PROP') if (atomic is not None) else (self.extract_atomicpred(atomic_s_),'PRED')
    return atomic

`extract_atomicpred(self, atomprep_s_)` ¶

1	`extract_atomicpred(atomprep_s_:AbstractString)`

This function returns two matches; [1] for the formula name which is a CAPITAL letter possibly followed by some digit sequence and [2] a string of variables for the formula.

This is bsed on the formula pattern; ∀xFxy, so where the variables are NOT separeted by commas in a parenthesized list of formula variables. I have changed this to the more readable and easier parsable format; ∀xF(x,y) with possibly nested formulas like; ∀x∀yF(x,G(x,y)). The matrix is a nested expression of predicate formulas.

So the quantified matrix always starts with a capital letter followed by '(...)' a single parenthesized group with content. This content can be anything from a single prop constant 'a' to a fully nested set of parameters. What is returned in the second regex group does not have the surrounding paranthesis.

Source code in modalogic\parser\formulaparser.py

def extract_atomicpred(self, atomprep_s_:str):
    """
        extract_atomicpred(atomprep_s_:AbstractString)

    This function returns two matches; [1] for the formula name which is a CAPITAL letter possibly followed by some digit sequence and [2] a string of variables for the formula.

    This is bsed on the formula pattern; ∀xFxy, so where the variables are NOT separeted by commas in a parenthesized list of formula variables. I have changed this to the more readable and easier parsable format; ∀xF(x,y) with possibly nested formulas like; ∀x∀yF(x,G(x,y)). The matrix is a nested expression of predicate formulas.

    So the quantified matrix always starts with a capital letter followed by '(...)' a single parenthesized group with content. This content can be anything from a single prop constant 'a' to a fully nested set of parameters. What is returned in the second regex group does not have the surrounding paranthesis.
    """
    m = re.match(r"^([A-Z]\d*)\(([A-Za-z)\d,(]*)\)$", atomprep_s_)
    return  re.collect(m.captures) if m is not None else None

`extract_atomicprop(self, atomprop_s_)` ¶

1	`extract_atomicprop(atomprop_s_:AbstractString)`

This function extracts a propositional constant from the formula.

Source code in modalogic\parser\formulaparser.py

def extract_atomicprop(self, atomprop_s_:str):
    """
        extract_atomicprop(atomprop_s_:AbstractString)

    This function extracts a propositional constant from the formula.
    """
    r1 = re.compile(r"^([a-z]\d*)$")
    m = r1.findall(atomprop_s_)
    return m if m is not [] else None

`extract_binarysubfs(self, norm_s_, mc_, norm_lut_)` ¶

1	`extract_binarysubfs(norm_s_:AbstractString, mc_:String, norm_lut_:Vector{String})`

This function will break the formula over the main connective and replace the content placeholders with their string from the lookup table and returns the two subformula strings.

These will be passed on to create the two new LogicFormula objects. The LogicFormula objects recurse until we have an atomic formula.

Source code in modalogic\parser\formulaparser.py

def extract_binarysubfs(self, norm_s_:str, mc_:str, norm_lut_:list[str]):
    """
        extract_binarysubfs(norm_s_:AbstractString, mc_:String, norm_lut_:Vector{String})

    This function will break the formula over the main connective and replace the content placeholders with their string from the lookup table and returns the two subformula strings.

    These will be passed on to create the two new LogicFormula objects. The LogicFormula objects recurse until we have an atomic formula.
    """

    # if startswith("∀",norm_s_) # dealing with quantified and need to keep scope together
    #     norm_s_ = replace(norm_s_,"∀"=>"∀(")
    #     norm_s_ *= ")"
    # elseif startswith("∃",norm_s_) # dealing with quantified and need to keep scope together
    #     norm_s_ = replace(norm_s_,"∃"=>"∃(")
    #     norm_s_ *= ")"
    # end

    nrt = norm_s_.replace(mc_, "%split")
    if len(norm_lut_) > 0:
        for (idx,entry) in enumerate(norm_lut_):
            li = "%$idx"
            nrt = nrt.replace(li, entry)

    subl, subr = nrt.split("%split")
    return subl, mc_, subr

`extract_inparens(self, parens_f_s_)` ¶

1	`extract_inparens(parens_f_s_:String)`

This function is used to extract the content from a formula that uses superfluous parenthesis around the content.

Source code in modalogic\parser\formulaparser.py

def extract_inparens(self, parens_f_s_:str):
    """
        extract_inparens(parens_f_s_:String)

    This function is used to extract the content from a formula that uses superfluous parenthesis around the content.
    """
    m = re.match(r"^\((.*)\)$", parens_f_s_)
    return re.collect(m.captures) if m is not None else None

`extract_quantsubfs(self, quant_f_s_)` ¶

1	`extract_quantsubfs(quant_f_s_:AbstractString)`

This function is used to extract the scope content of a quantified formula which is considered everything after the quantifier and the variable where the content can be another quantified formula.

Source code in modalogic\parser\formulaparser.py

def extract_quantsubfs(self, quant_f_s_:str):
    """
        extract_quantsubfs(quant_f_s_:AbstractString)

    This function is used to extract the scope content of a quantified formula which is considered everything after the quantifier and the variable where the content can be another quantified formula.
    """
    m = re.match(r"^([∀|∃])([xyzwvutsr]\d*)(.+$)",quant_f_s_)
    if m is not None:
        ms = re.collect(m.captures)
        return ms[1], m[2], m[3]
    return None

`extract_unarysubfs(self, negmod_f_s_)` ¶

1	`extract_unarysubfs(negmod_f_s_:String)`

This function will take a formula string that starts with the ¬ character and then extracts the remainder for the formula from the string.

The ¬ formula is either: ¬p or ¬(A) so always what follows is what we're after. In the latter case we need to remove the superfluous parens which is another parse-compile option. Operators can be: ¬ ◻ ⬨ !!

Source code in modalogic\parser\formulaparser.py

def extract_unarysubfs(self, negmod_f_s_:str):
    """
        extract_unarysubfs(negmod_f_s_:String)

    This function will take a formula string that starts with the ¬ character and then extracts the remainder for the formula from the string.

    The ¬ formula is either: ¬p or ¬(A) so always what follows is what we're after. In the latter case we need to remove the superfluous parens which is another parse-compile option. Operators can be: ¬ ◻ ⬨ !!
    """
    if bool(re.search('¬', negmod_f_s_)):
        start = negmod_f_s_.find('¬')+1
        neg_form_s = negmod_f_s_[start:len(negmod_f_s_)]
        return neg_form_s , 'NEG'
    elif bool(re.search('[◻|⬨]', negmod_f_s_)):
        # got modal formula
        nstrt_b = str.find('◻', negmod_f_s_)
        nstrt_d = str.find('⬨', negmod_f_s_)
        start = str.index('¬')+1
        modal_type =  'BOX' if nstrt_b != -1 else 'DIAMOND'
        neg_form_s = negmod_f_s_[start:-1]
        return neg_form_s, modal_type
        raise Exception("NOT SUPPORTED YET : NO MODEL OPERATOR SUPPORT JUST YET")

`getmainconnective(self, norm_s_)` ¶

1	`getmainconnective(norm_s_:AbstractString)`

For a binary expression we need to get the highest-priority connective from the string so we can split the normalized expression around it and rehydrate the norm_strin from the lookup table.

Source code in modalogic\parser\formulaparser.py

def getmainconnective(self, norm_s_:str):
    """
        getmainconnective(norm_s_:AbstractString)

    For a binary expression we need to get the highest-priority connective from the string so we can split the normalized expression around it and rehydrate the norm_strin from the lookup table.
    """
    if bool(re.search('⟺', norm_s_)):
        return "⟺"
    elif bool(re.search('⟹', norm_s_)):
        return "⟹"
    elif bool(re.search('⩔', norm_s_)):
        return "⩔"
    elif bool(re.search('⩓', norm_s_)):
        return "⩓"
    else:
        return None

`getpredicatename(self, curindex, terms_s)` ¶

1	`getpredicatename(curindex,terms_s)`

This function extracts the predicate name from the character string when processing a predicate function atomic formula.

Source code in modalogic\parser\formulaparser.py

def getpredicatename(self, curindex,terms_s):
    """
        getpredicatename(curindex,terms_s)

    This function extracts the predicate name from the character string when processing a predicate function atomic formula.
    """
    if curindex > len(terms_s):
        return (curindex, None)

    start = curindex
    predname = ""

    # for now we'll assume a valid predicate terms string
    while curindex < len(terms_s) and terms_s[curindex] not in ",)(%":
        curindex += 1

    # if we ran to the length of the file and not a stop-character get to length
    if curindex == len(terms_s) and terms_s[curindex] not in ",)(%":
        predname = terms_s[start:curindex]
    elif curindex == len(terms_s) and terms_s[curindex] not in ",)(%":
        predname = terms_s[start:curindex-1]
    else:
        predname = terms_s[start:curindex-1]    
    return (curindex,predname)

`hide_formula_in_parens(self, formula_s_)` ¶

1	`hide_formula_in_parens(formula_s_:AbstractString)`

This function will take a formula string and normalize it into a atom-string or a single or binary normalized formula. All toplevel content of a parameter pair is placed in a lookup table that aligns with the replacement code in the normalizaed string.

Source code in modalogic\parser\formulaparser.py

def hide_formula_in_parens(self, formula_s_:str):
    """
        hide_formula_in_parens(formula_s_:AbstractString)

    This function will take a formula string and normalize it into a atom-string or a single or binary normalized formula. All toplevel content of a parameter pair is placed in a lookup table that aligns with the replacement code in the normalizaed string.
    """
    lut = [] # the lookup table for the operands
    lutIndex = 0 # the starter index 1-based
    parenDepth = 0 # detecting outer-most bracket completion
    normstr = "" # the expresion string normalized

    # the norm string is all the top-level text outside of the parens content. There is always
    # only a negated, quantified, modal or binary expression. The first have a single parent and
    # the binary always has two paren contents
    # norm_s "p"            =>   p
    # norm_s "¬p"           =>   ¬p
    # norm_s "p⩓(B⟹C)"          =>   p⩓%1  in the lut, lut[1] == "B⟹C"
    # norm_s "(A⟺B)⩓(B⟹C)"     =>   %1⩓%2  in the lut, lut[1] == A⟺B and lut[1] == "B⟹C"
    #
    # however complex the input function string is there is always only a negated, atomic, quantified,
    # modal or binary expression.

    for c in formula_s_: # g over every character in the formula string

        if c == '(':
            parenDepth = parenDepth + 1 # only at == 0 are we at outer loop
            if parenDepth == 1:  # only at paren level 1 do we get the lut
                lutIndex = len(lut)+1
                lut.append("") # will only ever max 2 times
                normstr = normstr * "%$lutIndex"
                continue

        if c == ')':
            parenDepth = parenDepth - 1

        if parenDepth == 0:
            if c != ')': # we're in norm string level don't append last ')' chr
                normstr = normstr + c  # just append to the symbol lookup            
        else: # we're in lut mode append to lookup string
            lut[lutIndex] = lut[lutIndex] + c


    # HACK: for the ns F%1 or any {capital-letter,%} combination the capital-letter must be brought
    # into the LUT and removed from the norm-string. I will revert the whole approach to the minimal
    # format -- which will require a deep change in the parsing of the function parameters but for
    # now I'm just patching the hide_formula method to support the parenthesized formula syntax!!
    r1 = re.compile(r"([A-Z]\d*)\%(\d)+")
    mall=r1.findall(normstr)
    for plut in mall:
        predfname = plut[1]
        lutindx = int(plut[2])
        lut[lutindx] = predfname + "(" + lut[lutindx] + ")"
    normstr=normstr.replace(r"([A-Z]\d*)\%(\d)+", r"%\2")

    r2 = re.compile(r"([∃∀][a-z]\d*)\%(\d)")
    quantifs=r2.findall(normstr)  # removed start string from regex !!
    for qlut in quantifs:
        qidx = qlut[2]
        lutindx = int(qidx)
        lut[lutindx] = "(" + lut[lutindx] + ")"

    return normstr, lut

`initModality(self)` ¶

Source code in modalogic\parser\formulaparser.py

def initModality(self):
    """
    """
    pass

`is_atomic(srel, atom_s)` ¶

1	`is_atomic(atom_s_:AbstractString):Bool`

This function returns true when the provided string is a single letter plus an optional number of digits which make the string a propositional constant or a predicate formula with the parenthesized syntax like ""F(y,H(i,j))"" where the formulas have an single uppercase letter with optional digits and every parameters (prop constants or other predicate formulas) are separarted by commas.

Source code in modalogic\parser\formulaparser.py

def is_atomic(srel, atom_s:str)-> bool:
    """
        is_atomic(atom_s_:AbstractString):Bool

    This function returns true when the provided string is a single letter plus an optional number of digits which make the string a propositional constant or a predicate formula with the parenthesized syntax like ""F(y,H(i,j))"" where the formulas have an single uppercase letter with optional digits and every parameters (prop constants or other predicate formulas) are separarted by commas.
    """

    isAtomicProp = bool(re.search('^([a-z]\d*)$', atom_s)) # a propositional constant

    isAtomicPred = bool(re.search('^([A-Z]\d*)\(([A-Za-z)\d,(]*)\)$', atom_s)) # a predicate function

    isAtomic = isAtomicProp or isAtomicPred

    return isAtomic

`is_negormodal(self, negmod_s_)` ¶

1	`is_negormodal(negmod_s_:AbstractString):Bool`

This is a simplistic form for the test and only asserts that the formula starts with a modal operator or a negation operator followed by a valida variable. It ignores all that follows this prefix.

Source code in modalogic\parser\formulaparser.py

def is_negormodal(self, negmod_s_:str) -> bool:
    """
        is_negormodal(negmod_s_:AbstractString):Bool

    This is a simplistic form for the test and only asserts that the formula starts with a modal operator or a negation operator followed by a valida variable. It ignores all that follows this prefix.
    """
    isNegMod = bool(re.search('^[¬|◻|⬨]', negmod_s_))
    return isNegMod

`is_quantified(self, quant_s_)` ¶

1	`is_quantified(quant_s_:AbstractString):Bool`

This is a simplistic form for the test and only asserts that the formula starts with a quantifier followed by a valid variable. It ignores all that follows this prefix.

Source code in modalogic\parser\formulaparser.py

def is_quantified(self, quant_s_:str) -> bool:
    """
        is_quantified(quant_s_:AbstractString):Bool

    This is a simplistic form for the test and only asserts that the formula starts with a quantifier followed by a valid variable. It ignores all that follows this prefix.
    """
    isQuant = bool(re.search('^([∀|∃])([xyzwvutsr]\d*)(.+$)', quant_s_))
    return isQuant

`isTseitinLiteral(self)` ¶

Source code in modalogic\parser\formulaparser.py

def isTseitinLiteral(self):
    """
    """
    pass

`parseInput(self, expression)` ¶

Parses an argument with premises or a single conclusion expression.

Parameters:

Name	Type	Description	Default
`expression`	`str`	the expression to parse	required

Exceptions:

Type	Description
`ArgumentDoubleTurnStileException`	raised if too many turnstiles are found

Returns:

Type	Description
`(list[premises,conclusion])`	is a list of premise formula objects formula object.

Source code in modalogic\parser\formulaparser.py

def parseInput(self, expression:str):
    """Parses an argument with premises or a single conclusion expression.

    Args:
        expression (str):the expression to parse

    Raises:
        ArgumentDoubleTurnStileException: raised if too many turnstiles are found

    Returns:
        (list[premises,conclusion]): <premises> is a list of premise formula objects <conclusion> formula object.
    """

    parts = expression.split("|=")
    if (len(parts) > 2):
        raise ArgumentDoubleTurnStileException(
            "You can't use more than one turnstile")

    if len(parts) == 2:
        # split premises by commas that are not in parentheses:
        temp = self.hideSubStringsInParens(parts[0])
        nstr = temp[0]
        subStringsInParens = temp[1]
        premiseStrings = nstr.split(',')
        for idx, ps in enumerate(premiseStrings):
            # restore substrings:
            for ssp in subStringsInParens:
                ps = ps.replace(f"%{idx}", ssp)
            prem_f = self.parseFormula(ps)
            self.premises.append(prem_f)
            prem_o = self.premises[idx]
            prem_os = f"{prem_o}"
            prems_len = len(self.premises)
            # TODO: figure out a string serialization
            #tinylog.log_i([f"=== premise {prems_len}: {prem_o}]"])

    # process thelist of premises formulas
    self.conclusions =self.parseFormula(parts[-1])
    return self.premises, self.conclusions

`parser_copy(self)` ¶

This function creates and returns a deep copy of the provided parser. This is used when variables are introduced which can happen when constructing the CNN as well as during the tree construction.

Source code in modalogic\parser\formulaparser.py

def parser_copy(self):
    """This function creates and returns a deep copy of the provided parser. This 
    is used when variables are introduced which can happen when constructing the 
    CNN as well as  during the tree construction.
    """
    return copy.deepcopy(self)

`parseterms(self, terms_string)` ¶

1	`parseterms(terms_string:AbstractString)`

This function takes the terms collection of a predicate formula and constructs a hierarchical data structure that captures the full predicate function structure of the terms collection.

The function basically slides over the input string from start to finish and for each extracted term object it will return the advanced index pointer and the new term object. There are three functions actove: 1) the parseterms function takes the input string, 2) parsetermsrecurse that will slide over the string and accumulates the structure in the provided root note and 3) a utility function to extract the names of predicate constants and functions.

Source code in modalogic\parser\formulaparser.py

def parseterms(self, terms_string:str):
    """
        parseterms(terms_string:AbstractString)

    This function takes the terms collection of a predicate formula and constructs a hierarchical data structure that captures the full predicate function structure of the terms collection.

    The function basically slides over the input string from start to finish and for each extracted term object it will return the advanced index pointer and the new term object. There are three functions actove: 1) the parseterms function takes the input string, 2) parsetermsrecurse that will slide over the string and accumulates the structure in the provided root note and 3) a utility function to extract the names of predicate constants and functions.
    """
    terms_node = PredicateTermNode('root', ".")
    self.parseTermsRecurse(1, terms_string, terms_node)
    return terms_node

`prepare_formula(self, prep_formula, from_ascii=True)` ¶

This function will remove all the white space from the input string and it replaces all brackets types with parenthesis and remove parens from the around the quantifiers: (∀x)F(x) => ∀xF(x). It optionally will do a symbol replacement on the string first if it is written in ascii text.

Parameters:

Name	Type	Description	Default
`prep_formula`	`str`	the formula expression to clean up	required
`from_ascii`	`bool`	indicates an ascii expression to convert. Defaults to True.	`True`

Returns:

Type	Description
`str`	str:cleaned up expression string for the whole argument.

Source code in modalogic\parser\formulaparser.py

def prepare_formula(self, prep_formula:str, from_ascii:bool=True) -> str:
    """This function will remove all the white space from the input string and it replaces all brackets types with parenthesis and remove parens from the around the quantifiers: (∀x)F(x) => ∀xF(x). It optionally will do a symbol replacement on the string first if it is written in ascii text.

    Args:
        prep_formula (str): the formula expression to clean up
        from_ascii (bool, optional): indicates an ascii expression to convert. Defaults to True.

    Returns:
        str:cleaned up expression string for the whole argument.
    """
    # 1. convert all asii representations to UTF symbols
    # 2: remove all whitespace
    # 3: replace all ']['with ')('
    # 4: remove parentheses around quantifiers: (∀x)Fx => ∀xFx

    cf = prep_formula
    if from_ascii:
        cf = ExpressionRewriter.toSymbols(cf)
    cf = re.sub(r"\s+", r"",cf)
    cf = re.sub(r"\[", r"(",cf)
    cf = re.sub(r"\]", r")",cf)
    cf = re.sub(r"\(([∀∃]\w\d*)\)", r"\1",cf)
    return cf

`registerExpression(self, ex, ex_type, arity)` ¶

The purpose of this function is to create the symbol table for the for parser of the sentence or argument. There is a symbols-list where we simply add the expression and a lookup table for the ex.

Source code in modalogic\parser\formulaparser.py

def registerExpression(self, ex, ex_type, arity):
    """ The purpose of this function is to create the symbol table for the
    for parser of the sentence or argument. There is a symbols-list where
    we simply add the expression and a lookup table for the ex.
    """

    # test if the expression with ex is already encountered
    if ex not in self.expression_types.keys():
        self.symbols.append(ex)
    elif (self.expression_types[ex] != ex_type):
        errmsg = f"don\'t use {ex} as both {self.expression_types[ex]} and {ex_type}"
        raise errmsg
    self.expression_types[ex] = ex_type
    self.arities[ex] = arity
    pass

`stripAccessibilityClauses(self)` ¶

Source code in modalogic\parser\formulaparser.py

def stripAccessibilityClauses(self):
    """
    """
    pass

`tidyFormula(self, formula)` ¶

This function will clean up the expression by changing the '[' chars to parens and remove parens from the around the quantifiers: (∀x)Fx => ∀xFx

Source code in modalogic\parser\formulaparser.py

def tidyFormula(self, formula):
    """ This function will clean up the expression by changing the '[' chars to 
    parens and remove parens from the around the quantifiers: (∀x)Fx => ∀xFx
    """
    cleaned_formula = formula

    # 1: remove all whitespace
    cleaned_formula = re.sub(r'\s+', "", cleaned_formula)
    # 2: replace all '['with ')'
    cleaned_formula = cleaned_formula.replace("[", "(").replace("]", ")")
    # 3:  remove parentheses around quantifiers: (∀x)Fx => ∀xFx
    cleaned_formula = re.sub(r"\(([∀∃]\w\d*)\)", r"\g<1>", cleaned_formula)

    return cleaned_formula

`translateFromModal(self)` ¶

Source code in modalogic\parser\formulaparser.py

def translateFromModal(self):
    """
    """
    pass

`translateToModal(self)` ¶

Source code in modalogic\parser\formulaparser.py

def translateToModal(self):
    """
    """
    pass

`version()` `classmethod` ¶

This function returns the currect SKU version of the parser feature of the package.

Returns:

Type	Description
`str`	the SKU version as semantic version string.

Source code in modalogic\parser\formulaparser.py

@classmethod
def version(self):
    """This function returns the currect SKU version of the parser feature of the package.

    Returns:
        str: the SKU version as semantic version string.
    """
    return "0.0.1"

`symboltable` ¶

The SymbolTable module maintains information about the variables that the parser encounters dusing the parsing process of arguments and expressions.

`ParserSymbol` ¶

The ParserSymbol has information about an object that was retrieved from the argument or expression string.

`SymbolTable` ¶

The SymbolTable is the structure that maintains information about all the symbols that are in use for the evaluation of the tableau of an argument. This is of crucial importance during the expansion of the delta and gamma nodes in the tableau. It is key off the expression string which is either a propositional constant or a function name+sigature.

`newname(self, candidates)` ¶

This function will cycle over the candidates letter string to return a new symbol name for the given type and if it has gone through them once it will start adding sequence numbers for each new cycle. Not implemented very intelligently ;-)

Source code in modalogic\parser\symboltable.py

def  newname(self, candidates:str) -> str:
    """
    This function will cycle over the candidates letter string to return a new symbol name for the given type and if it has gone through them once it will start adding sequence numbers for each new cycle. Not implemented very intelligently ;-)
    """
    for c in candidates:
        if c not in self.symbols: return c

    seqno = 1
    newnamefound=False
    while not newnamefound:
        for c in candidates:
            nn=f"{c}{seqno}"
            if nn not in self.symbols: return nn                
        seqno = seqno + 1
    return ""

`SymbolTableEntry` ¶

The SymbolTableEntry structure is a simple data struct to main information about symbols used in expressions during an argument evaluation.

Last update: 2021-07-02

ModaLogic Architecture Documentation¶

The Parser Feature¶

argumentparser ¶

ArgumentParser ¶

prepare_formula(self, prep_formula, from_ascii=True) ¶

process_argument(self) ¶

formulaparser ¶

FormulaParser ¶

extract_atomic(self, atomic_s_) ¶

extract_atomicpred(self, atomprep_s_) ¶

extract_atomicprop(self, atomprop_s_) ¶

extract_binarysubfs(self, norm_s_, mc_, norm_lut_) ¶

extract_inparens(self, parens_f_s_) ¶

extract_quantsubfs(self, quant_f_s_) ¶

extract_unarysubfs(self, negmod_f_s_) ¶

getmainconnective(self, norm_s_) ¶

getpredicatename(self, curindex, terms_s) ¶

hide_formula_in_parens(self, formula_s_) ¶

initModality(self) ¶

is_atomic(srel, atom_s) ¶

is_negormodal(self, negmod_s_) ¶

is_quantified(self, quant_s_) ¶

isTseitinLiteral(self) ¶

parseInput(self, expression) ¶

parser_copy(self) ¶

parseterms(self, terms_string) ¶

prepare_formula(self, prep_formula, from_ascii=True) ¶

registerExpression(self, ex, ex_type, arity) ¶

stripAccessibilityClauses(self) ¶

tidyFormula(self, formula) ¶

translateFromModal(self) ¶

translateToModal(self) ¶

version() classmethod ¶

symboltable ¶

ParserSymbol ¶

SymbolTable ¶

newname(self, candidates) ¶

SymbolTableEntry ¶

`argumentparser` ¶

`ArgumentParser` ¶

`prepare_formula(self, prep_formula, from_ascii=True)` ¶

`process_argument(self)` ¶

`formulaparser` ¶

`FormulaParser` ¶

`extract_atomic(self, atomic_s_)` ¶

`extract_atomicpred(self, atomprep_s_)` ¶

`extract_atomicprop(self, atomprop_s_)` ¶

`extract_binarysubfs(self, norm_s_, mc_, norm_lut_)` ¶

`extract_inparens(self, parens_f_s_)` ¶

`extract_quantsubfs(self, quant_f_s_)` ¶

`extract_unarysubfs(self, negmod_f_s_)` ¶

`getmainconnective(self, norm_s_)` ¶

`getpredicatename(self, curindex, terms_s)` ¶

`hide_formula_in_parens(self, formula_s_)` ¶

`initModality(self)` ¶

`is_atomic(srel, atom_s)` ¶

`is_negormodal(self, negmod_s_)` ¶

`is_quantified(self, quant_s_)` ¶

`isTseitinLiteral(self)` ¶

`parseInput(self, expression)` ¶

`parser_copy(self)` ¶

`parseterms(self, terms_string)` ¶

`prepare_formula(self, prep_formula, from_ascii=True)` ¶

`registerExpression(self, ex, ex_type, arity)` ¶

`stripAccessibilityClauses(self)` ¶

`tidyFormula(self, formula)` ¶

`translateFromModal(self)` ¶

`translateToModal(self)` ¶

`version()` `classmethod` ¶

`symboltable` ¶

`ParserSymbol` ¶

`SymbolTable` ¶

`newname(self, candidates)` ¶

`SymbolTableEntry` ¶