=ADD=
=reftype=
14
=number=
99-34
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-34.ps.gz
=year=
1999
=month=
10
=author=
Konev; Boris
=title=
Metavariable Method for Natural Deduction within {\em Theorema}
=abstract=
The problem of finding of terms that have to be substituted during the proof
search in places of quantified variables (like in the case of $\exists xP(x)$)
is a well-known problem of automated theorem proving. In this paper we present
an efficient implementation of the metavariable method for Natural Deduction.
We show how to find terms when the proof search is performed in \AND{}-\OR{}
tree like structures; the implementation does not depend on the search
strategy and allows integration with other provers.
=keywords=
Theorema, automated reasoning, natural deduction, metavariable
=sponsor=
INTAS project 96-760