Geodesic
Heuristic for Avoiding Skolemization in Theorem Proving
Publications de l'Institut Mathématique, _N_S_38 (1985) no. 52, p. 207 .

Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

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 : 68G15 
@article{PIM_1985_N_S_38_52_a26,
     author = {Irena Pevac},
     title = {Heuristic for {Avoiding} {Skolemization} in {Theorem} {Proving}},
     journal = {Publications de l'Institut Math\'ematique},
     pages = {207 },
     publisher = {mathdoc},
     volume = {_N_S_38},
     number = {52},
     year = {1985},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/PIM_1985_N_S_38_52_a26/}
}
TY  - JOUR
AU  - Irena Pevac
TI  - Heuristic for Avoiding Skolemization in Theorem Proving
JO  - Publications de l'Institut Mathématique
PY  - 1985
SP  - 207 
VL  - _N_S_38
IS  - 52
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PIM_1985_N_S_38_52_a26/
LA  - en
ID  - PIM_1985_N_S_38_52_a26
ER  - 
%0 Journal Article
%A Irena Pevac
%T Heuristic for Avoiding Skolemization in Theorem Proving
%J Publications de l'Institut Mathématique
%D 1985
%P 207 
%V _N_S_38
%N 52
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PIM_1985_N_S_38_52_a26/
%G en
%F PIM_1985_N_S_38_52_a26
Irena Pevac. Heuristic for Avoiding Skolemization in Theorem Proving. Publications de l'Institut Mathématique, _N_S_38 (1985) no. 52, p. 207 . http://geodesic.mathdoc.fr/item/PIM_1985_N_S_38_52_a26/