Parsers¶

class logics.utils.parsers.standard_parser.StandardParser(language, parse_replacement_dict=None, unparse_replacement_dict=None, infix_cts=None, comma_separator=',', inference_separator='/', derivation_step_separator=';', two_sided_sequent_separator='⇒', n_sided_sequent_separator='|')¶

Parser for propositional languages.

Parsers serve for transforming strings into Formula, Inference, Sequent, etc. and vice-versa, thus handling objects of those types more easily and less cumbersombly. See below for some examples.

Parameters:

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
parse_replacement_dict (dict, optional) – Dictionary of the form ({string: string, …}). See below for an explanation
unparse_replacement_dict (dict, optional) – Same as the above parameter
infix_cts (list of str, optional) – The list of constants that will be written in infix notation
comma_separator (str, optional) – Character (preferrably of len 1) used to separate the premises or separate the conclusions within an inference
inference_separator (str, optional) – Character (preferrably of len 1) used to separate between the premises and conclusions in an inference
derivation_step_separator (str, optional) – Character (preferrably of len 1) used to separate the components of a derivation step
two_sided_sequent_separator (str, optional) – Character (preferrably of len 1) used to separate the two sides of a two-sided sequent
n_sided_sequent_separator (str, optional) – Character (preferrably of len 1) used to separate the sides of an n-sided sequent

Examples

Let us first define a language (say, one containing only conjunction and negation as constants)

>>> from logics.classes.propositional import Language
>>> language = Language(atomics=['p', 'q', 'r'],
...                     constant_arity_dict={'~': 1, '∧': 2},
...                     sentential_constants=['⊥', '⊤'],
...                     metavariables=['A', 'B', 'C'],
...                     context_variables=['Γ', 'Δ', 'Σ', 'Λ', 'Π', 'Θ'])

We now define a parser for that language

>>> from logics.utils.parsers.standard_parser import StandardParser
>>> parser = StandardParser(language=language,
...                         parse_replacement_dict= {'&': '∧', ' and ': '∧', 'not ': '~',
...                                                  '==>': '⇒', 'Gamma': 'Γ', 'Delta': 'Δ'},
...                         # Note the whitespaces in the keys above, in ' and ' and 'not '
...                         infix_cts=['∧'], comma_separator=',', inference_separator='/',
...                         derivation_step_separator=';', two_sided_sequent_separator='⇒',
...                         n_sided_sequent_separator='|')

With that, we can do things like the following:

>>> f = parser.parse('~(p and not q)')
>>> f
['~', ['∧', ['p'], ['~', ['q']]]]
>>> type(f)
<class 'logics.classes.propositional.formula.Formula'>
>>> parser.unparse(f)
'~(p ∧ ~q)'
>>> i = parser.parse('(p / p) // (q / p & not p)')
>>> i
([([['p']] / [['p']])] // [([['q']] / [['∧', ['p'], ['~', ['p']]]])])
>>> type(i)
<class 'logics.classes.propositional.inference.Inference'>
>>> parser.unparse(i)
'(p / p) // (q / p ∧ ~p)'
>>> s = parser.parse('Gamma, A ==> Delta')
>>> s
[['Γ', ['A']], ['Δ']]
>>> type(s)
<class 'logics.classes.propositional.proof_theories.sequents.Sequent'>
>>> parser.unparse(s)
'Γ, A ⇒ Δ'

There are some pre-instantiated parsers for common languages (such as classical language and its fragments), e.g:

>>> from logics.utils.parsers import classical_parser
>>> classical_parser.parse('p iff not (p or q)')
['↔', ['p'], ['~', ['∨', ['p'], ['q']]]]

The instances are documented below in this document.

Suppose you want to use the classical parser, but want to use '⊃' and '≡' instead of '→' and '↔'. Instead of redefining everything again (the language, parser, every model theory and proof theory, etc…) you can just add a rule to parse_replacement_dict and another to unparse_replacement_dict as follows:

>>> classical_parser.parse_replacement_dict.update({'⊃': '→', '≡': '↔'})
>>> classical_parser.unparse_replacement_dict.update({'→': '⊃', '↔': '≡'})
>>> # You can now use '⊃' and '≡' as arguments to the parser
>>> f = classical_parser.parse('(p ≡ q) and (q ⊃ r)')
>>> # Internally, the formula is still stored with '→' and '↔'
>>> f
['∧', ['↔', ['p'], ['q']], ['→', ['q'], ['r']]]
>>> # When unparsing, you will see what you want ('⊃' and '≡')
>>> classical_parser.unparse(f)
'(p ≡ q) ∧ (q ⊃ r)'

parse(string, replace=True)¶

Parses a string and returns an object of the appropriate type (Formula, Inference or Sequent).

Will automatically detect the type of object you want to build. If any of the sequent separators are present, will return a Sequent; elif the inference separator is present, will return an Inference; otherwise it will return a Formula.

Inferences (of any level) should come between parentheses, e.g. '((p / q), (q / r) // p) /// (// (/ p))' (outermost ones can be avoided).

This is to avoid ambiguity, since, for example 'p / q, r / s //' could be read as '(p / q, r) (/ s) //', '(p / q), (r / s) //' or '(p /) (q, r / s) //')

unparse(logics_object, first_iteration=True)¶

Takes an object (Formula, Inference or Sequent) and returns a readable string version of it.

The first_iteration parameter is for recursion purposes and should not be altered.

parse_derivation(string, natural_deduction=False)¶

Parse an axiomatic or natural deduction derivation

string must come in the following format:

'''p → ((p → p) → p); ax1
(p → ((p → p) → p)) → ((p → (p → p)) → (p → p)); ax2
p → (p → p); ax1
((p → (p → p)) → (p → p)); mp; [1, 2]
p → p; mp; [3, 4]'''

That is, it is a multiline string such that each step comes in a different line. Components of a step must be separated by the derivation_step_separator. If the on_steps and open_suppositions are not specified, will assume they are an empty list.

Can also parse Natural deduction derivations, with steps have one extra element for the open suppositions, e.g.: "p → p; mp; [3, 4]; [1, 2]". For that, set natural_deduction to True.

Instances¶

logics.utils.parsers.classical_parser¶: Parser for classical languages (with or without sentential constants and infinite atomics and metavariables). Its parse_replacement_dict looks as follows:

parse_replacement_dict = {
    # For negation
    '¬': '~',
    'not ': '~',

    # For conjunction
    '&': '∧',
    ' and ': '∧',

    # For disjunction
    'v': '∨',  # The key is a letter v, so if you plan to use this parser dont use that as an atomic of Language
    ' or ': '∨',

    # For conditional
    ' then ': '→',
    '-->': '→',
    'if ': '',  # if you write 'if p then q' it will just leave 'p then q'

    # For biconditional
    ' iff ': '↔',
    '<->': '↔',

    # For the semantic hammer
    '|=': '/',

    # Sentential constants
    'falsum': '⊥',
    'Falsum': '⊥',
    'bottom': '⊥',
    'Bottom': '⊥',
    'verum': '⊤',
    'Verum': '⊤',
    'Top': '⊤',
    'top': '⊤',

    # For sequent calculi
    '==>': '⇒',
    'Gamma': 'Γ',
    'Delta': 'Δ',
    'Sigma': 'Σ',
    'Pi': 'Π',
    'Theta': 'Θ',
    'Lambda': 'Λ',
}

logics.utils.parsers.modal_parser¶: Similar to the parser above, but modal languages. Adds the following replacement rules:

modal_replacement_dict.update({
    'box ': '□',
    'Box ': '□',
    'necessary ': '□',
    'nec ': '□',
    '◻': '□',
    'diamond ': '◇',
    'Diamond ': '◇',
    'possible ': '◇',
    'pos ': '◇'
})

logics.utils.parsers.LFI_parser¶: Similar to the classical parser, but contains two new unary connectives • and ◦. Adds the following replacement rules:

LFI_replacement_dict.update({
    "inc ": "•",
    "inconsistent ": "•",
    "con ": "◦",
    "consistent ": "◦",
    "°": "◦",
})