search

kiniry / Mobius

4 stars 8 forks source link

[ escjava-Feature Requests-117 ] Check all theorems in the new PVS logic #189

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

!html

Reply to: noreply@sort.ucd.ie }}} {{{ Feature Requests item #117, was opened at 2005-08-08 20:24 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=444&aid=117&group_id=97

Category: Completeness Improvements Group: CVS HEAD

Status: Closed Resolution: Out of Date Priority: 3 Submitted By: Joseph Kiniry (jkiniry) Assigned to: Joseph Kiniry (jkiniry) Summary: Check all theorems in the new PVS logic

Initial Comment: The original Simplify object logic (called "escjava_logic") has been encoded in PVS. This logic has had sorts applied to it and several basic built-in PVS theories have been used to simplify the logic significantly. This new logic is called "escjava2_logic" in ESCTools/docs/Escjava2-Logics/unsorted/. All the original axioms of the original logic have been converted into lemmas. We need to prove the lemmas with the new axiomisation to ensure that everything is kosher.

You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=444&aid=117&group_id=97 }}}

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:20:45 2007

added mailto line

This message has 0 attachment(s)

atiti commented 11 years ago

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted