diff --git a/pvs/socrates-mortal.pvs b/pvs/socrates-mortal.pvs
new file mode 100644
index 0000000..baf8781
--- /dev/null
+++ b/pvs/socrates-mortal.pvs
@@ -0,0 +1,13 @@
+socrates: THEORY
+BEGIN
+  man: TYPE
+  socrates: man
+  x: VAR man
+  mortal(x): boolean
+
+  menMortal: AXIOM
+    forall x: mortal(x)
+
+  socratesMortal: LEMMA
+    mortal(socrates)
+END socrates
diff --git a/pvs/sum-n.pvs b/pvs/sum-n.pvs
new file mode 100644
index 0000000..b693e8a
--- /dev/null
+++ b/pvs/sum-n.pvs
@@ -0,0 +1,14 @@
+sumn: THEORY
+BEGIN
+  n: VAR nat
+  sum(n): RECURSIVE nat =
+    (IF n = 0 THEN
+       0
+     ELSE
+       n + sum(n-1)
+     ENDIF)
+     MEASURE (λ n: n)
+
+  nnatsum: THEOREM
+    sum(n) = (n * (n+1)) / 2
+END sumn
diff --git a/pvs/sum-n3.pvs b/pvs/sum-n3.pvs
new file mode 100644
index 0000000..ebc1518
--- /dev/null
+++ b/pvs/sum-n3.pvs
@@ -0,0 +1,25 @@
+sum: THEORY
+BEGIN
+  n: VAR nat
+  f, g: VAR [nat -> nat]
+
+  sum(f, n): RECURSIVE nat =
+    IF n = 0
+      THEN 0
+      ELSE f(n-1) + sum(f, n - 1)
+    ENDIF
+   MEASURE n
+
+  sum_plus: LEMMA
+   sum((lambda n: f(n) + g(n)), n) = sum(f, n) + sum(g, n)
+
+  square(n): nat = n*n
+
+  sum_of_squares: LEMMA
+    6 * sum(square, n+1) = n * (n + 1) * (2*n + 1)
+
+  cube(n): nat = n*n*n
+
+  sum_of_cubes: LEMMA
+    4 * sum(cube, n+1) = n*n*(n+1)*(n+1)
+END sum
diff --git a/pvs/sum-tut.pvs b/pvs/sum-tut.pvs
new file mode 100644
index 0000000..6b1dd74
--- /dev/null
+++ b/pvs/sum-tut.pvs
@@ -0,0 +1,10 @@
+sumtut: THEORY
+  BEGIN
+    n: VAR nat
+
+    sum(n): RECURSIVE nat =
+      (IF n = 0 THEN 0 ELSE n + sum(n-1) ENDIF)
+      MEASURE (LAMBDA n:n)
+ 
+    closed_form: THEOREM sum(n) = n * (n + 1)/2
+  END sumtut