PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.) Vol. 38(52), pp. 207213 (1985) 

HEURISTIC FOR AVOIDING SKOLEMIZATION IN THEOREM PROVINGIrena PevacMatematicki institut SANU, Beograd, YugoslaviaAbstract: 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
