Forse si desidera provare un metodo di prova semiautomatico. Per esempio, se si dispone di una specifica Java degli algoritmi di Prim e Kruskal, che si basa in modo ottimale sullo stesso modello di grafico, è possibile utilizzare lo KeY Prover per dimostrare l'equivalenza dell'algoritmo.
La parte cruciale è formalizzare l'obbligo di prova in Dynamic Logic (questa è un'estensione della logica del primo ordine con tipi e mezzi di esecuzione simbolica dei programmi Java). La formula per dimostrare potrebbe corrispondere il seguente (discutibile) modello:
\forall Graph g. \exists Tree t.
(<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)
Ciò esprime che per tutti i grafici, entrambi gli algoritmi terminano e il risultato è lo stesso albero.
Se sei fortunato e la tua formula (e le implementazioni algoritmiche) sono corrette, allora KeY può dimostrarlo automaticamente per te. In caso contrario, potrebbe essere necessario istanziare alcune variabili quantificate che rendono necessario ispezionare l'albero delle prove precedente.
Dopo aver provato la cosa con KeY, puoi essere felice di aver imparato qualcosa o provare a ricostruire una prova manuale dalla prova KeY - questo può essere un compito noioso dal momento che KeY conosce un sacco di regole specifiche per Java che non sono facili da comprendere Tuttavia, forse si può fare qualcosa come estrarre una disgiunzione Herbrand dai termini che KeY ha usato per istanziare i quantificatori esistenziali sul lato destro delle sequenze nella dimostrazione.
Beh, penso che Key è uno strumento interessante e sempre più persone devono abituarsi a dimostrare codice Java critica utilizzando strumenti come questo;)
provare mathoverflow.com. Penso che avrai più fortuna lì – Toad
Non penso che questo tipo di domanda sia per cosa sia mathoverflow.com. –