Files

 master

/

provers

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

giomasce

Fix exists elimination rule conversion.

Jun 4, 2019

43e97d5 · Jun 4, 2019

History

History

/

provers

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
tstp		tstp	Rename setmm.h -> setmm_loader.h.	May 19, 2019
fof.cpp		fof.cpp	Implement (good part of) FOF conversion to Metamath.	May 21, 2019
fof.h		fof.h	Implement (good part of) FOF conversion to Metamath.	May 21, 2019
fof_to_mm.cpp		fof_to_mm.cpp	Fix a few problems with equality.	Jun 4, 2019
fof_to_mm.h		fof_to_mm.h	Fix a few problems with equality.	Jun 4, 2019
gapt.cpp		gapt.cpp	Fix exists elimination rule conversion.	Jun 4, 2019
gapt.h		gapt.h	Introduce ND proof parsing.	May 14, 2019
ndproof.cpp		ndproof.cpp	Generalize fof_to_mm architecture a little bit.	Jun 3, 2019
ndproof.h		ndproof.h	Generalize fof_to_mm architecture a little bit.	Jun 3, 2019
ndproof_to_mm.cpp		ndproof_to_mm.cpp	Fix exists elimination rule conversion.	Jun 4, 2019
ndproof_to_mm.h		ndproof_to_mm.h	Finish conversion of propositional rules.	May 24, 2019
sat.cpp		sat.cpp	Make namespace std explicit everywhere.	Mar 15, 2018
sat.h		sat.h	New WffSat prover finally at work!	Mar 9, 2018
setmm.cpp		setmm.cpp	Refactor code for ND proofs.	May 22, 2019
setmm.h		setmm.h	Refactor code for ND proofs.	May 22, 2019
subst.cpp		subst.cpp	Guard temp variable releasing through temp_stacked_allocator.	May 20, 2019
subst.h		subst.h	Experiments.	Mar 15, 2018
uct.cpp		uct.cpp	Guard temp variable releasing through temp_stacked_allocator.	May 20, 2019
uct.h		uct.h	Guard temp variable releasing through temp_stacked_allocator.	May 20, 2019
wff.cpp		wff.cpp	Add type tag to PTEngine.	May 20, 2019
wff.h		wff.h	Follow change from enable_create to virtual_enable_create.	Oct 29, 2018
wffblock.cpp		wffblock.cpp	Make namespace std explicit everywhere.	Mar 15, 2018
wffblock.h		wffblock.h	First attempt, not working, at full proof generation with SAT refutat…	Mar 8, 2018
wffsat.cpp		wffsat.cpp	Continue working.	Sep 20, 2018
wffsat.h		wffsat.h	Prepare a working Wff prover via SAT refutation.	Mar 8, 2018
z3prover.cpp		z3prover.cpp	Rename setmm.h -> setmm_loader.h.	May 19, 2019
z3prover2.cpp		z3prover2.cpp	Rename setmm.h -> setmm_loader.h.	May 19, 2019
z3prover3.cpp		z3prover3.cpp	Rename setmm.h -> setmm_loader.h.	May 19, 2019
z3prover3.h		z3prover3.h	Experiments with Z3.	Oct 30, 2018
z3resolver.cpp		z3resolver.cpp	Fix compatibility with different versions of Z3.	Dec 13, 2018
z3resolver.h		z3resolver.h	Fix compatibility with different versions of Z3.	Dec 13, 2018
View all files