Parsers

class logics.utils.parsers.predicate_parser.PredicateParser(language, parse_replacement_dict, unparse_replacement_dict=None, infix_cts=None, infix_pred=None, infix_func=None, comma_separator=',', inference_separator='/', derivation_step_separator=';')

Parser for predicate languages.

Extends StandardParser. Has two additional parameters to specify infix predicates and functions. Also includes some changes in the format of the valid input:

  • Atomics must be given in format "R(a, b, c)" for prefix predicates, or "a = b" for infix predicates

  • Infix predicate formuale must come without outer parentheses, e.g. "(a = b)" is not well formed

  • Outermost parentheses in infix function terms can be ommited, e.g. both "0+(0+0)" and "(0+(0+0))" are ok

  • Infix predicates and function symbols CANNOT be given in prefix notation

  • Quantified formulae come in format ∀x A or ∀x ∈ T A - Do not add extra parentheses to the quantified formula

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

  • infix_pred (list of str, optional) – The list of predicates that will be written in infix notation

  • infix_func (list of str, optional) – The list of function symbols 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

Examples

>>> from logics.instances.predicate.languages import real_number_arithmetic_language
>>> from logics.utils.parsers.predicate_parser import PredicateParser
>>> replacement_dict = {
...     '¬': '~', 'not ': '~',
...     '&': '∧', ' and ': '∧',  # notice the spaces before and after 'and'
...     'v': '∨',  ' or ': '∨',
...     ' then ': '→', '-->': '→', 'if ': '',  # 'if p then q' it will convert to 'p then q'
...     ' iff ': '↔', '<->': '↔',
...     'forall ': '∀', 'exists ': '∃', ' in ': '∈'
... }
>>> real_number_arithmetic_parser = PredicateParser(language=real_number_arithmetic_language,
...                                                 parse_replacement_dict=replacement_dict,
...                                                 infix_cts=['∧', '∨', '→', '↔'],
...                                                 infix_pred=['=', '<', '>'], infix_func=['+', '*', '**'])
>>> real_number_arithmetic_parser.parse("0.5 + 0.5 = 1")
['=', ('+', '0.5', '0.5'), '1']
>>> f = real_number_arithmetic_parser.parse("1 + 1 = 2 or exists x x + 1 = 2")
>>> f
['∨', ['=', ('+', '1', '1'), '2'], ['∃', 'x', ['=', ('+', 'x', '1'), '2']]]
>>> type(f)
<class 'logics.classes.predicate.formula.PredicateFormula'>
>>> real_number_arithmetic_parser.unparse(f)
'1 + 1 = 2 ∨ ∃x x + 1 = 2'
>>> # Infix predicates and function symbols cannot be given in prefix notation
>>> real_number_arithmetic_parser.parse("=(+(1,1),2)")
Traceback (most recent call last):
...
logics.classes.exceptions.NotWellFormed: String  is not a valid term

Examples with a predefined parser for a language with prefix predicates and function symbols (see below for more predefined instances):

>>> from logics.utils.parsers.predicate_parser import classical_predicate_parser
>>> classical_predicate_parser.parse("R(a, b) or P(f(a))")
['∨', ['R', 'a', 'b'], ['P', ('f', 'a')]]
>>> classical_predicate_parser.parse("forall x ~P(x)")
['∀', 'x', ['~', ['P', 'x']]]
>>> classical_predicate_parser.parse("forall x in f(a) (if ~P(x) then P(x))")
['∀', 'x', '∈', ('f', 'a'), ['→', ['~', ['P', 'x']], ['P', 'x']]]
parse_term(string, replace=True)

Parses an individual term

If replace is True, will apply the parse_replacement_dict to the string before parsing the term. Otherwise, it will not.

Examples

>>> from logics.utils.parsers.predicate_parser import realnumber_arithmetic_parser
>>> realnumber_arithmetic_parser.parse_term("1+1")
('+', '1', '1')
>>> realnumber_arithmetic_parser.parse_term("1+(1+2)")
('+', '1', ('+', '1', '2'))
>>> realnumber_arithmetic_parser.parse_term("(1+(1+2))")
('+', '1', ('+', '1', '2'))

Instances

logics.utils.parsers.predicate_parser.classical_predicate_parser

Parser for classical_function_language (see Language > Instances). Also works for the predicate languages without function symbols. Uses "forall "`, ``"exists " and " in " for quantified formulae.

logics.utils.parsers.predicate_parser.arithmetic_parser

Similar to the above example. Defined for arithmetic_language (see Language > Instances). Thus, has only 0 as individual constant (the rest of the numerals cannot be used). To refer to the rest of the natural numbers, you can use the s (successor) function.

logics.utils.parsers.predicate_parser.realnumber_arithmetic_parser

Identical to the parser defined above. Can use all the numerals (and floats, such as "0.5") as constants.