EMIS ELibM Electronic Journals PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 35(49), pp. 167--171 (1984)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home

EMIS Home

 		 

SOME HEURISTICS IN AUTOMATIC THEOREM PROVING

Dragos Cvetkovi\'c and Irena Pevac

Matematicki 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
© 2001--2002 ELibM and FIZ Karlsruhe / Zentralblatt MATH for the EMIS Electronic Edition