PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 38(52), pp. 207--213 (1985)
HEURISTIC FOR AVOIDING SKOLEMIZATION IN THEOREM PROVING
Irena PevacMatematicki institut SANU, Beograd, Yugoslavia
Abstract: Some further possibilities of the theorem prover of the system GRAPH -- 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