Applied Logic for Computer Scientists

Solutions of selected exercises (pdf)

Examples of Formalizations

1. Tutorial on Formal Reasoning with PVS given at Nat@Logic 2015

• Tutorial foils
• PVS exercises

2. Tutorial on Fomalization of Rewriting in PVS given at ISR 2014

• Tutorial foils
• PVS exercises

The NASA LaRC PVS library contains TRS, a complete library of term rewriting properties

3. Checking Sorting Algorithms (compressed library)

This library contains the classic sorting algorithms (mergesort, quicksort, insertion sort, etc) over lists and sequences of naturals

The NASA LaRC PVS library contains a version of sorting over non-interpreted sorted types

Recommended PVS complete tutorials:

• PVS for Computer Scientists 2017 held as a Tableaux/ITP/FroCoS tutorial in Brasília, 2017
• NASA/NIA PVS Class 2012 held in Hampton, 2012