> We did not get time to convert all the comments into code as is done > for some the new categories and domains in the trunk repository. > For example, from > > http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
Is there a way I could help in a pan-Axiom sort of way? For instance, would it be any help if I went through these categories and drew a diagram of their relationships? I realise diagrams like: http://www.axiom-developer.org/axiom-website/bookvol10.2full.html tend to quickly become unwieldy. But if the diagram was limited to pure algebras and split into operator and algebra categories, perhaps it might be more manageable? Or, would it be more practical to model it in one of the formal methods tools around, such as? * Formal specification program, * Formal development program, * Formal verification program, * Theorem provers I have no experience in using any of these programs but, when they came up in this thread I did some searches and they appear to be very powerful (I guess their limitations only become clear with experience)? At first glance CASL appears very powerful for axioms. quote from wiki page here. http://en.wikipedia.org/wiki/Specification_language "In the property-oriented approach to specification (taken e.g. by CASL), specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy - often just by their interrelationship. This is in contrast to so-called model-oriented specification in frameworks like VDM and Z, which consist of a simple realization of the required behaviour." So, if I understand correctly: CASL is good at theories (axiom categories). ACL2 is good at models of those theories (axiom domains). (or by Curry–Howard: proofs) I have not yet seen a program that is good at both. I get the impression that ACL2, after a very quick search on the web (so I may be wrong), does term rewriting and proofs but its input is not axioms but some sort of state machine defined in LISP? (I have not seen the light regarding LISP, but let not have that debate!). So I just wondered if anyone has had experience with any of these 'formal methods tools' and would there be any benefit in my attempting to learn one? (to experiment with specifying axioms or to experiment with term rewriting systems). Or would it be best to wait (hopefully not for the full 30 years) until you guys implement more of this stuff? Martin ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
