Libro · 2002 · Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel

Isabelle/HOL

Questo volume è un'introduzione autonoma alla dimostrazione interattiva nella logica di ordine superiore (HOL), utilizzando l'assistente alla prova Isabelle 2002. Rispetto alla documentazione esistente di Isabelle, fornisce un percorso diretto verso la logica di ordine superiore, che la maggior parte delle persone preferisce al giorno d'oggi. Salta la logica di primo ordine e minimizza la discussione sulla meta-teoria. È scritto per potenziali utenti piuttosto che per i nostri colleghi nel mondo della ricerca. Un'altra differenza rispetto alla documentazione precedente è che descriviamo la notazione degli script di prova di Markus Wenzel invece degli script di tattiche ML. Questi ultimi rendono più facile introdurre nuove tattiche al volo, ma praticamente nessuno lo fa. La sintassi dedicata di Wenzel è elegante, sostituendo ad esempio otto tattiche di semplificazione con un unico metodo, cioè simp, con le relative applicazioni. Il libro è suddiviso in tre parti. – La prima parte, Tecniche Elementari, mostra come modellare programmi funzionali nella logica di ordine superiore. I primi esempi riguardano liste e numeri naturali. La maggior parte delle dimostrazioni è lunga due passi, consistenti nell'induzione su una variabile scelta seguita dalla tattica auto. Ma anche questa parte elementare copre argomenti avanzati come la ricorsione annidata e mutua. – La seconda parte, Logica e Insiemi, presenta una raccolta di tattiche di livello inferiore che puoi utilizzare per applicare regole in modo selettivo. Descrive anche il trattamento di Isabelle/HOL di insiemi, funzioni e relazioni e spiega come definire insiemi in modo induttivo. Uno degli esempi riguarda la teoria del model checking, e un altro è tratto da un classico libro di testo sui linguaggi formali.