# HG changeset patch # User Oleksandr Gavenko # Date 1240047927 -10800 # Node ID a8482dddf447313388d26d07f26a7e493c2fc925 # Parent 72175e4fc06994c043aa757609c67dc077dbf009# Parent 1c0c9a83c06263186909012127e4241af3b33f66 merge diff -r 1c0c9a83c062 -r a8482dddf447 auto-proof.rst --- a/auto-proof.rst Thu Apr 16 10:46:54 2009 +0300 +++ b/auto-proof.rst Sat Apr 18 12:45:27 2009 +0300 @@ -1,5 +1,12 @@ -*- outline -*- +* Info/links. + +See + + http://en.wikipedia.org/wiki/Automated_theorem_proving + + * proofgeneral. $ sudo apt-get install proofgeneral @@ -65,3 +72,87 @@ See http://formalmath.tiddlyspot.com/ + +* ACL2. + +ACL2 (A Computational Logic for Applicative Common Lisp) is a software system +consisting of a programming language, an extensible theory in a first-order +logic, and a mechanical theorem prover. ACL2 is designed to support automated +reasoning in inductive logical theories, mostly for the purpose of software +and hardware verification. The input language and implementation of ACL2 are +built on Common Lisp. ACL2 is free, open source (GPL) software. + + $ sudo apt-get install acl2 + +See + + http://www.cs.utexas.edu/users/moore/acl2/ + http://en.wikipedia.org/wiki/ACL2 + +* PVS Specification and Verification System + +Old (1992). Many article in 199x. + +The system is implemented in Common Lisp, and is released under the GNU +General Public License (GPL). + +See + + http://pvs.csl.sri.com/ + http://en.wikipedia.org/wiki/Prototype_Verification_System + http://www-formal.stanford.edu/clt/ARS/Entries/pvs + +* The TPTP Problem Library for Automated Theorem Proving. + +The TPTP (Thousands of Problems for Theorem Provers) is a library of test +problems for automated theorem proving (ATP) systems. The TPTP supplies the +ATP community with: + + * A comprehensive library of the ATP test problems that are available today, + in order to provide an overview and a simple, unambiguous reference + mechanism. + * A comprehensive list of references and other interesting information for + each problem. + * Arbitrary size instances of generic problems (e.g., the N-queens problem). + * A utility to convert the problems to existing ATP systems' formats. + * General guidelines outlining the requirements for ATP system evaluation. + * Standards for input and output for ATP systems. + +The principal motivation for the TPTP is to support the testing and evaluation +of ATP systems, to help ensure that performance results accurately reflect the +capabilities of the ATP system being considered. A common library of problems +is necessary for meaningful system evaluations, meaningful system comparisons, +repeatability of testing, and the production of statistically significant +results. The TPTP is such a library. + +See + + http://www.cs.miami.edu/~tptp/ + +* SPASS. + +An Automated Theorem Prover for First-Order Logic with Equality. + +See + + http://www.spass-prover.org/index.html + +* Competition. + +See + + http://www.cs.miami.edu/~tptp/CASC/ + http://www.cs.albany.edu/~nvm/cade.html + +* Conference. + +IJCAR is a series of conferences on the topics of automated reasoning, +automated deduction, and related fields. It is organized semi-regularly as a +merger of other meetings. IJCAR replaces those independent conferences in the +years it takes place. The conference is organized by CADE Inc., and CADE has +always been one of the conferences partaking in IJCAR. + +See + + http://www.ijcar.org/ + http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning diff -r 1c0c9a83c062 -r a8482dddf447 bluetooth.rst --- a/bluetooth.rst Thu Apr 16 10:46:54 2009 +0300 +++ b/bluetooth.rst Sat Apr 18 12:45:27 2009 +0300 @@ -97,3 +97,10 @@ http://www.bluez.org/ bluez home page + +* Spec. + +See + + http://www.bluetooth.com/Bluetooth/Technology/Building/Specifications/ + diff -r 1c0c9a83c062 -r a8482dddf447 emacs.rst --- a/emacs.rst Thu Apr 16 10:46:54 2009 +0300 +++ b/emacs.rst Sat Apr 18 12:45:27 2009 +0300 @@ -7,25 +7,28 @@ know about line numbers and files – it just knows an error happened, and that’s it. -You have several options: +** Binary Search. - * Binary Search – select half of the file in a region, and M-x eval-region. - Depending on whether that causes the error or not, split this half or the - other half again, and repeat. +Select half of the file in a region, and M-x eval-region. Depending on whether +that causes the error or not, split this half or the other half again, and +repeat. + +** Elisp. - * Simplified Binary Search – add (error “No error until here”) in the - middle of your file. If you get the error “No error until here” when - reloading the file, move the expression towards the back of the file, - otherwise towards the front of the file. + - Use a keyboard macro that moves forward one expression (sexp) and evaluates + it. + - Try C-x check-parens. + - Set (setq debug-on-error t). + +** CLI. - * Use a keyboard macro that moves forward one expression (sexp) and - evaluates it. + $ emacs --no-init-file --no-site-file --debug-init + +** Simplified Binary Search. - * Try the command line switch --debug-init. - - * Should n’t (setq debug-on-error t) help? - - * Try check-parens. +Add (error “No error until here”) in the middle of your file. If you get the +error “No error until here” when reloading the file, move the expression +towards the back of the file, otherwise towards the front of the file. * Using edebug. diff -r 1c0c9a83c062 -r a8482dddf447 javascript.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/javascript.rst Sat Apr 18 12:45:27 2009 +0300 @@ -0,0 +1,17 @@ +-*- outline -*- + +* Inline in HTML. + + +

Hello!

+ + + +* Hot calc by Firefox. + +At URI type some thing like "javascript: 4+5"