Y at-il une bibliothèque pour effectuer le raisonnement automatisé

Question

Je veux écrire un programme qui peut faire un raisonnement déductif comme ça:

Pièces:

chats sont des oiseaux 1.All.

2.Chaque oiseau peut voler. Conclusion: Chaque chat peut voler. (Il est absurde que)

(Il est juste un exemple. En fait, il serait plus complexe que cela)

Le programme que je désire sera en mesure de recevoir une entrée de conclusion par l'utilisateur et vérifier si elle est valide en vertu donné locaux qui sont déjà stockés dans le programme et, si possible, en mesure de suggérer quelle conclusion serait valable. Donc, ma question, y a-t-il une bibliothèque qui peut fonctionner de cette façon pour moi?

Answer 1

Vous ne mentionnez pas de langue, donc je ne sais pas si ce que vous voulez vraiment c'est une bibliothèque. Ce que vous décrivez ressemble à théorème automatisé prouvant et donc vous pourriez bien faire pour enquêter sur ce sujet. Un théorème automatisé prouvant le langage - ou assistant de preuve interactif, ou ce que vous voulez - est Coq. Je ne l'ai pas utilisé mais la page Wikipedia est informative. J'ai essayé de rassembler une preuve simple mais franchement c'est un peu compliqué.

Une autre option est la programmation logique. PROLOG, par exemple, vous permettrait de faire quelque chose comme:

canfly(X) :- isbird(X). 
isbird(X) :- iscat(X). 
iscat(tom). 
?- canfly(tom). 
Yes