YAFOLPS (Yet Another First-Order Logic Problem Solver)
Semester project on mathematical logic of the fourth semester of Software Engineering, Department of System Programming, Faculty of Mathematics and Mechanics, St. Petersburg State University.
Goal
We must determine whether the input formula in First-Order Logic is a tautology or not. For this to be done, we have implemented the resolution method.
EBNF (Extended Backus–Naur form)
<Forall> ::= "!"
<Exists> ::= "?"
<LogicAnd> ::= "&"
<LogicOr> ::= "|"
<LogicNegation> ::= "-"
<LogicImplication> ::= ">"
<Top> ::= "^"
<Bottom> ::= "_"
<Char> ::= [a-z] | [A-Z] | [0-9] | "_"
<Var> ::= [A-Z] (<Char>)*
<Term> ::= <Var> | [a-z] (<Char>)* "(" ((<Term> ",")* <Term>) ")"
<Quantifier> ::= <Forall> | <Exists>
<LogicOperation> ::= <LogicAnd> | <LogicOr> | <LogicImplication>
<PredicateSymbol> ::= [a-z] (<Char>)* "(" ((<Term> ",")* <Term>) ")"
<Singleton> ::= <Top> | <Bottom> | <PredicateSymbol>
<Formula> ::= <Singleton> | "(" <Formula> ")"
| <Formula> <LogicOperation> <Formula>
| <Quantifier> <Var> "(" <Formula> ")"
Usage
stack build && stack exec -- YAFOLPS-exe <args>
Args
--input-file filename / --i filename -- Reads a formula from a file. Without specifying this option reads a formula from standard input.
--print-formula / -f -- Prints the formula that have been read.
--print-ast / -a -- Prints the AST of the formula.
--print-ssf / -s -- Prints the SSF of the negated formula.
--print-solution / -r -- Prints "VALID" if is the formula is a tautology, otherwise prints "NOT VALID".
Examples
stack build && stack exec -- YAFOLPS-exe --i examples/1.txt -fas
--Prints formula, AST and SSF
stack build && stack exec -- YAFOLPS-exe --i examples/1.txt -r
-- Prints "NOT VALID"
stack build && stack exec -- YAFOLPS-exe --i examples/2.txt -r
-- Prints "NOT VALID"
stack build && stack exec -- YAFOLPS-exe --i examples/3.txt -r
-- Prints "NOT VALID"
stack build && stack exec -- YAFOLPS-exe --i examples/4.txt -r
-- Prints "VALID"
stack build && stack exec -- YAFOLPS-exe --i examples/Top.txt -r
-- Prints "VALID"
stack build && stack exec -- YAFOLPS-exe --i examples/Bottom.txt -r
-- Prints "VALID"
Tests
stack test
--Prints results on the Hilbert's axioms