|
Come afferma [[Lorenzo Magnani]], nell'ambito della ''computer science'', ad esempio, ha insegnato alle macchine come imitare ragionamenti umani molto complessi<ref>[http://www.raiscuola.rai.it/lezione-embed/logica/4298/default.aspx ''Magnani: logica e possibilità'']</ref>, ad esempio con la [[bisimulazione]], cioè modelli di Kripke che usano un [[Sistema a transizione di stati]] al posto dei mondi possibili, per decidere la correttezza e la terminazione con successo di un programma informatico<ref name=":0">[https://plato.stanford.edu/entries/logic-modal/#DeoLog James Garson, ''Modal Logic''], su ''Stanford Encyclopedia of Philosophy'', First published Tue Feb 29, 2000; substantive revision Tue May 27, 2014</ref>.<br />
AlNel 2020, nell'applicazione del calcolo proposizionale sono noti elaboratori capaci di validare una dimostrazione di logica formale completa di tutti i passi logici, regole di calcolecalcolo applicate e relative assunzioni, ma non sono noti elaboratori capaci di elaborare autonomamente una dimostrazione, intesa come derivazione di una conclusione a partire da un insieme di una o più [[formula ben formata|formule ben formute]] assunte come premesse. In altre parole, l'elaboratore meccanico, elettronico o meccatronico è a posteriori in grado di confermare la correttezza o non correttezza di una dimostrazione eseguita da agenti umani, ma non è capace di eseguire una dimostrazione in modo tale da sostituirsi o superare l'operatore umano in tale tipo di ragionamento logico deduttivo.<ref>Edward J. Lemmon, ''Elementi di logica con gli esercizi risolti'', Giuseppe Laterza editore, cap. 1-''La logica proposizionale'', p. 43, ISBN 978-88-420-2772-0. Citazione: ''I calcoli aritmetici possono essere generati oltre che controllati, meccanicamente, mentre fin qui non abbiamo trovato alcun modo meccanico di generare prove - anche se, una volta scoperte, una macchina potrebbe certamente verificarne la validità.''</ref> Tale possibilità non è però stata esclusa a livello teoretico, data l'assimilazione della logica proposizionale al calcolo matematico numerico e letterale, già eseguito dagli elaboratori, e data la similitudine fra il formalismo di quest'ultima e quello della logica matematica.
== Modalità aletiche ==
|
