[Index] || [Contents] || [Grades] Tue Aug 5 11:45:01 PDT 2003

- Links to resources on Formal Methods
- : References
- : Logics
- : Tutorials and Classes
- : Tools
- : Books
- : Research
- : Jokes
- : Other
- : Glossary
- : Other
- Index of defined terms etc.

- PC::=
*Propositional Calculus*, foundation of nearly all other logics formulae are constructed from atomic propositions by operators acting like*and*,*or*,*if_then*,*not*, etc. - LPC::=
*Lower Predicate Calculus*, A predicate is a property of objects in a Universe of Discourse. Predicate calculus includes*PC*but defines special atomic propositions and additional operators*for all*,*for some*, etc. - LTL::=
*Linear Temporal Logic*. - Temporal_Logic::=
*Logic for expressing changing properties*, for example [ tl.html ] - CTL::=
*Compter Tree Logic*,*PC*with 8 new*modal*operators that quantify possible and necessary futures.If you can handle Dutch.... [ http://turing.wins.uva.nl/~jaspars/animations/ ] ( EN = /\, NIET= not, OF = \/ , alsdan = if_then, desda=iff, noch = not iff)

(Proofs): [ A0840257.html ]

(Tableaux): Research [ http://i12www.ira.uka.de/TABLEAUX/ ] , Notes [ Semantic Tableaux in logic_2_Proofs ] , and Cheat Sheet [ semtab.jpg ] Math [ contents.cgi ]

(MATHS): [ http://www.csci.csusb.edu/dick/maths/ ]

(Prolog): Programming in Logic: [ prolog.html ]

(Verification): TOny Hoare starts the ball rolling in the 1960s: [ 363235.363259 ]

(OBDDs): Examples of OBDDs [ http://indy4.fdl.cc.mn.us/obdd/ ] and other DDs: [ demo.html ]## Tutorials and Classes

(LICS web tutor):*LICS*has a tutorial: [ index.html ] [ home.html ]Paul Black and Anne Sobel presented: [ formaltut.html ]

## Tools

(SMV): http://www.csci.csusb.edu/dick/cs656/smvOne popular tool for computer people is the Prototype Verification System:

- PVS::= See http://pvs.csl.sri.com/,
at SRI.

(SPIN): A tool that checks sytems expressed in*Promela*to see if the meet*LTL*specifications: [ whatispin.html ]

(Promela): Process or Protocol Meta Language: [ promela.htm ] , The Concise Promela Reference.

(prolog): [ project2.html ]## Books

(textbook):*LICS*Logic, proofs by trees:

- Richard Jeffreys
- Formal Logic: It's Scope and Limits
- McGraw-Hill Education

## Research

## Jokes

## Other

(Math for profit): [ nf20020122_8839.htm ][ ideas.html ]

## Glossary

- LICS::="Logic In Computer Science", [ http://www.cis.ksu.edu/~huth/lics/ ]
- TBA::="To Be Announced".
## Other

(LISP): [ lisp.html ]

(TeX): [ comp.text.TeX.html ]*. . . . . . . . . ( end of section Links to resources on Formal Methods)*<<Contents | Index>>

- CTL (Definition)
- LICS (Definition)
- LICS web tutor (Label)
- LISP (Label)
- LPC (Definition)
- LTL (Definition)
- Math for profit (Label)
- MATHS (Label)
- OBDDs (Label)
- PC (Definition)
- prolog (Label)
- Prolog (Label)
- Promela (Label)
- Proofs (Label)
- PVS (Definition)
- SMV (Label)
- SPIN (Label)
- Tableaux (Label)
- TBA (Definition)
- Temporal_Logic (Definition)
- textbook (Label)
- TeX (Label)
- Verification (Label)