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 predicatesInfix predicate formuale must come without outer parentheses, e.g.
"(a = b)"
is not well formedOutermost parentheses in infix function terms can be ommited, e.g. both
"0+(0+0)"
and"(0+(0+0))"
are okInfix 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 only0
as individual constant (the rest of the numerals cannot be used). To refer to the rest of the natural numbers, you can use thes
(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.