Identifiant pérenne de la notice : 246093692
Notice de type
Notice de regroupement
Note publique d'information : Dans cette these, nous presentons un nouveau systeme d'inference pour la logique du
premier ordre appele hypotheses domains system (h.d.s.). Ce systeme d'inference, destine
a une utilisation en enseignement de la geometrie, a pour objectifs : - de mettre
en uvre des schemas de raisonnement naturels pour l'utilisateur, - de prendre en compte
la negation de la logique du premier ordre et d'assurer la completude des deductions,
- d'offrir la possibilite de produire des informations utiles a l'utilisateur si une
preuve echoue. Le systeme h.d.s. Est constitue de quatre regles d'inference qui operent
sur ce que nous appelons des litteraux etendus. Le caractere explicable des preuves
obtenues par h.d.s. Resulte de l'interpretation intuitive de ces litteraux etendus
et de ces regles d'inference. Nous montrons la consistance et la completude du systeme
d'inference et discutons des aspects lies a la calculabilite. Le systeme est compare
a d'autres approches existantes dont le systeme modified problem reduction format
de plaisted qu'il etend de facon significative. Les capacites abductives du systeme,
completes selon le pouvoir d'expression autorise par les litteraux etendus, sont detaillees.
Un demonstrateur base sur le systeme h.d.s. A ete mis en uvre en prolog iv et experimente
dans le cadre de la preuve de proprietes geometriques. Pour resoudre les problemes
d'efficacite, plusieurs strategies, dependantes ou non du domaine d'application, ont
ete concues et integrees. La non remise en cause par ces strategies des proprietes
theoriques, notamment completude du systeme, est justifiee. Enfin, l'utilisation d'une
evaluation sur un modele numerique pour guider la recherche des preuves est decrite,
et ses limites actuelles presentees.
paprika.idref.fr
data.idref.fr
Documentation
