Skip to content

Formulas and Grammars

Parsing formulas

In Mathesis, formulas are represented as objects. Formulas are parsed from strings using grammars (languages, syntax). mathesis.grammars.BasicGrammar is a basic grammar with a standard set of symbols for propositional and quantified logic:

  • ¬ for negation, ∧ for conjunction, ∨ for disjunction, → for conditional.
  • Arbitrary symbols are allowed for atomic formulas.

For example, ¬(A→C) is parsed as a negation of a conditional of two atomic formulas A and C.

from mathesis.grammars import BasicGrammar

grammar = BasicGrammar()

fml = grammar.parse("¬(A→C)")

print(fml, repr(fml))

¬(A→C) Neg[Cond[Atom[A], Atom[C]]]

The symbols option allows you to customize some symbols used in the grammar.

from mathesis.grammars import BasicGrammar

grammar = BasicGrammar(symbols={"conditional": "⊃"})

fml = grammar.parse("¬(A⊃C)")

print(fml, repr(fml))

¬(A→C) Neg[Cond[Atom[A], Atom[C]]]

It accepts a list of formulas as well.

from mathesis.grammars import BasicGrammar

grammar = BasicGrammar()

fmls = grammar.parse(["¬(A→C)", "B∨¬B", "(((A∧B)))"])

print([str(fml) for fml in fmls], repr(fmls))

['¬(A→C)', 'B∨¬B', 'A∧B'] [Neg[Cond[Atom[A], Atom[C]]], Disj[Atom[B], Neg[Atom[B]]], Conj[Atom[A], Atom[B]]]

Advanced

Constructing formula objects directly

mathesis.forms.Formula is the base class for all formulas.

from mathesis.forms import Negation, Conjunction, Disjunction, Conditional, Atom

fml = Negation(Conditional(Atom("A"), Atom("C")))

print(fml, repr(fml))

¬(A→C) Neg[Cond[Atom[A], Atom[C]]]

New connectives can be defined by subclassing Formula.

Custom grammars

While there is no restriction in the way that a formula string is translated into a formula object, by default Mathesis uses lark for parsing. Using lark, you can define arbitrary grammars in EBNF (Extended Backus-Naur Form) notation. For example, here is a simple grammar for first-order classical logic:

from mathesis.grammars import Grammar

class MyGrammar(Grammar):
    grammar_rules = r"""
?fml: conjunction
    | disjunction
    | conditional
    | negation
    | universal
    | particular
    | atom
    | _subfml

PREDICATE: /\w+/ | "⊤" | "⊥"
TERM: /\w+/

atom : PREDICATE ("(" TERM ("," TERM)* ")")?
negation : "¬" _subfml
conjunction : (conjunction | _subfml) "∧" _subfml
disjunction : (disjunction | _subfml) "∨" _subfml
conditional : _subfml "→" _subfml

_unary : negation | necc | poss | universal | particular
_subfml : "(" fml ")" | _unary | atom

%import common.WS
%ignore WS
""".lstrip()