FOL Grammar

This wiki page is an overview of Skeditor's FOL Grammar rules.

terms and formulas

terms may consist of variables (e.g. a, b, valueX), numbers (e.g. 1, -15, 987), scientific numbers (e.g. 1E-42), arithmetic operations (see below) and functions (see below).

formulas may consist of predicates (e.g. #p(t), #p()), quantifiers and logical operations (see below). TODO

order of operations

All arithmetic operators except for ^ are left-associative (i.e., a+b+c equlas (a+b)+c, whereas a^b^c equals a^(b^c)). All logical operators except <- and <-> are right-associative.

arithmetic operations

Basic mathmatical symbols can be used similar to other common grammars.

simple term
(a + b) - c

power example
a^b

power of terms
(a + b)^((a*b)-c)

Overview

Operation	Syntax
addition	+
substraction	-
multiplication	*
division	/
power	^

comparison operations

Operations to compare single variables or numbers/scientific numbers and terms may look like the following example.

term comparison
(a + b) > (c * 3)

single value comparison
a != 3

Overview

Operation	Syntax
equals, not equals	=, !=
greater than, smaller than	>, <
greater or equals, smaller or equals	>=, <=

functions

In this grammar, function calls without or with several parameters are allowed. Note that function parameters and return type are numbers.

Example of a simple function
f()

with multiple parameters being passed
someMethod(parameter1, parameter2)

qualified identifiers are allowed
SomeClass.someMethod(someParameter)

Some common mathematical functions are already specified in the grammar. Known functions have the prefix \ to be recognized and checked on number of parameters. The following table shows the currently known functions.

Overview of known functions

Operation	Syntax
sinus, cosinus, tangens	\sin(x), \cos(x), \tan(x)
maximum, minimum	\max(x, y), \min(x,y)
absolute value	\abs(x)

quantifiers

The quantifiers for all and exists may contain a single or multiple members.

simple example for quantifiers
\forall (X) (x < y)

example with more than one variable
\forall (x, y, z) (x + y < z)

quantifiers may be contained in the domain of an other quantifier
\forall (x) (\exists(y) (x > y))

Overview

Operation	Syntax
For all	\forall
Exists	\exists

logical operations

This grammar provides basic logical operations to build formulas like
(a ∧ b ∧ c) → ¬(a ∨ b)

with the following syntax
(#a() & #b() & #c()) -> !(#a() | #b())

Examples

Operation	Syntax
and, logical and	&, &&
or, logical or	|, ||
implication	->
logical equivalence	<->
true, false	\true, \false