PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 35(49), pp. 167--171 (1984)
SOME HEURISTICS IN AUTOMATIC THEOREM PROVING
Dragos Cvetkovi\'c and Irena PevacMatematicki institut SANU, Beograd, Yugoslavia
Abstract: We propose two heuristics in automatic theorem proving: an analogy heuristic and a heurietic for detecting the logical equivalence of formulas. The first heuristic tries to establish an analogy between some subtheories of two non-analogous theories and to prove in this way a formula in one theory using a theorem in the second one. The second heuristic is related to the case when one should establish the logical equivalence of two formulas by instantiation of definitions. The structure of the definition set is represented by a digraph and a digraph coloring language is used.
Classification (MSC2000): 68G15
Full text of the article:
Electronic fulltext finalized on: 3 Nov 2001. This page was last modified: 22 Aug 2002.
© 2001 Mathematical Institute of the Serbian Academy of Science and Arts