EMIS ELibM Electronic Journals PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 38(52), pp. 207--213 (1985)

Previous Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home

EMIS Home

 		 

HEURISTIC FOR AVOIDING SKOLEMIZATION IN THEOREM PROVING

Irena Pevac

Matematicki institut SANU, Beograd, Yugoslavia

Abstract: Some further possibilities of the theorem prover of the system GRAPH [2]--[5] are described. Instead of skolemization of a formula, we transform the subgoal into an equivalent form or into a stronger subgoal with less quantifiers, in a human like manner. A heuristic is proposed how to choose, among several possibilities, a stronger subgoal which would be proved more easily. Although an incomplete method, it is suitable for interactive work since human behavior is imitated. If machine's choice is not suitable, the user can appropriately modify the transformation.

Classification (MSC2000): 68G15

Full text of the article:

Electronic fulltext finalized on: 2 Nov 2001. This page was last modified: 16 Nov 2001.

© 2001 Mathematical Institute of the Serbian Academy of Science and Arts
© 2001 ELibM for the EMIS Electronic Edition