GitHub - lagenar/fol: Program to transform First order logic formulas into clause normal form

lagenar / fol Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Program to transform First order logic formulas into clause normal form

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 53 Commits
COPYING		COPYING
Makefile		Makefile
OCamlMakefile		OCamlMakefile
README		README
cnl.ml		cnl.ml
cnl.mli		cnl.mli
error.ml		error.ml
fol.ml		fol.ml
fol.mli		fol.mli
lexer.mll		lexer.mll
main.ml		main.ml
parser.mly		parser.mly
util.ml		util.ml

Repository files navigation

Dependencias:
 -- ocaml
 -- make

Compilación:

make

Para crear un ejecutable nativo:
make nc

Ejecutar:
./fol

Formato:
Variables comienzan con una letra mayúscula, funciones y predicados con minúscula.
El or lógico es "|"
El and es "&"
Implica es "=>"
Not es "~"

Ejemplos de fórmulas:

forall[X,Y](p(X,Y))
exists[Y](forall[X](P(X,Y) & ~Q(X,f(Y))))
~p(X) => e(Y)
exists[X](barber(X) & forall[Y]((~shaves(Y,Y) => shaves(X,Y)) & (shaves(X,Y) => ~shaves(Y,Y))))