Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Miguel Á. Vallejo @ LSI
I'm interested in authomatic theorem proving (ATP), now I'm working in ATP for
first order logics with built-in equality (FOLE).
We have implementated a programming kernel called DEDAM (deduction
abstract machine) which is composed basically by two well known foundations:
the WAM (Warren Abstract Machine) and the Substitution trees (Graf RTA'95).
We have instaciated this kernel in two ATP´s for purely equational logic.
With the first one, called Barcelona, we have participated
in the 13th CADE competition. The second one,called Fiesta,
participated in the 14th CADE competition obtaining the third place in its
category.
Another research line that we have followed is the compilation for completed
(sub)theories, to get this aim we have used the WAM methods to compile but we
needed to do it also with the Substitution trees, so, we have developed a
special strategy to compile them.
Now are working to gain efficience in matching and re-write procedures by the
use of specialized Substitution Trees. In a short time we will develop an
ATP for general FOL clauses.
If you want a copy of our papers on this research field or an executable item
of our systems or our bench-marks, e-mail me.
Economy And Social-Political Section: