| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| alternative label
| - Hypotheses domains system, an inference system which constructs natural proofs and which produces missing hypotheses
|
| dc:subject
| - Informatique
- Thèses et écrits académiques
- Proof theory
- Sciences appliquees
- Inference rule
- Theorie preuve
- Abduction
- Calculabilite
- Completeness
- Completude
- Computability
- Consistance
- Consistency
- Demonstration theoreme
- First order logic
- Logique ordre 1
- Prolog
- Regle inference
- Theorem proving
- automatique theorique
- systemes
|
| preferred label
| - Hypotheses domains system, un système d'inférence pour la construction de preuves naturelles et la production d'hypothèses
|
| Language
| |
| Subject
| |
| dc:title
| - Hypotheses domains system, un système d'inférence pour la construction de preuves naturelles et la production d'hypothèses
|
| Degree granting institution
| |
| note
| - 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.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
