Études-Mathématique/Extension pour simplifier l'application des règles simples

From Lazi wiki
Jump to: navigation, search

Question

Peut-on définir une extension permettant d'utiliser plus simplement les règles simples, pour éviter de fournir tous les arguments de l'instance d'une telle règle ?

Étude

On pourrait ne fournir que la conclusion à déduire. La traduction d'une telle déduction consiste à chercher dans la liste des règles simples une règle pouvant déduire cette conclusion et à en déduire par matching les valeurs des variables de la règle. Pour les règles où toutes les variables ne sont pas dans la conclusion, on pourrait ajouter l'information de la valeur de ces variables.

Pour la validité ou le calcul des conditions, la règle utilise la même fonction de recherche que pour la traduction.

Réponse

Oui on peut. L'instance est la conclusion avec éventuellement des informations en plus. Voir l'étude.