{ "info": { "author": "Jonathan Jacky", "author_email": "jon@u.washington.edu", "bugtrack_url": null, "classifiers": [ "Development Status :: 5 - Production/Stable", "Environment :: Console", "Intended Audience :: Education", "Intended Audience :: Science/Research", "License :: OSI Approved :: GNU General Public License (GPL)", "Natural Language :: English", "Operating System :: MacOS :: MacOS X", "Operating System :: Microsoft :: Windows", "Operating System :: OS Independent", "Operating System :: POSIX :: Linux", "Programming Language :: Python :: 2.3", "Topic :: Scientific/Engineering :: Mathematics" ], "description": "F L i P : Logical Framework in Python\n=====================================\n\n**Flip** is a logical framework written in Python. A logical framework is\na library for defining logics and writing applications such as theorem\nprovers. One Flip application is a proof checker for entering and\nediting proofs in natural deduction style. Here is some output from\nthe checker, generated from a Python proof script:\n::\n\n Kaye ex. 9.12, ~Ax.P(x) |- Ex.~P(x) (0) Comment\n ~Ax.P(x) (1) Given\n |~Ex.~P(x) (2) Assumption\n ||Let x be arbitrary (3) New variable for subproof\n |||~P(x) (4) Assumption\n |||Ex.~P(x) (5) E-Introduction (4)\n |||F (6) Contradiction (5) (2)\n ||~~P(x) (7) Reductio Ad Absurdum (4) (6)\n ||P(x) (8) Not-Elimination (7)\n |Ax.P(x) (9) A-Introduction (3) (8)\n |F (10) Contradiction (9) (1)\n ~~Ex.~P(x) (11) Reductio Ad Absurdum (2) (10)\n Ex.~P(x) (12) Not-Elimination (11)\n\nThe checker can use different logics; Flip comes with several. You\ncan add another logic, or add axioms and derived rules, by writing a\nmodule in Python. Python is both the object language and the\nmetalanguage. Formulas, inference rules, and entire proofs are Python\nexpressions. Prover commands are Python functions. The Python\ninterpreter itself is the only user interface to the proof checker\napplication. (It is not necessary to know much Python to use the\nchecker.)\n\nFlip was undertaken as a Python programming exercise. It is not\nintended to compete with industrial-strength theorem provers such as HOL,\nnor with nicely-designed educational provers such as Jape.\nThat said, the checker is quite capable of working the examples and\nexercises in university-level textbooks on logic for computer science or\nmathematics, such as Kaye, Huth and Ryan, and Bornat.", "description_content_type": null, "docs_url": null, "download_url": "http://staff.washington.edu/jon/flip/www/download.html", "downloads": { "last_day": -1, "last_month": -1, "last_week": -1 }, "home_page": "http://staff.washington.edu/jon/flip/www/", "keywords": "logical framework python theorem prover proof checker natural deduction", "license": "GNU General Public License (GPL)", "maintainer": null, "maintainer_email": null, "name": "FLiP", "package_url": "https://pypi.org/project/FLiP/", "platform": "UNKNOWN", "project_url": "https://pypi.org/project/FLiP/", "project_urls": { "Download": "http://staff.washington.edu/jon/flip/www/download.html", "Homepage": "http://staff.washington.edu/jon/flip/www/" }, "release_url": "https://pypi.org/project/FLiP/1.2/", "requires_dist": null, "requires_python": null, "summary": "F L i P : Logical Framework in Python", "version": "1.2" }, "last_serial": 337318, "releases": { "1.0": [], "1.1": [ { "comment_text": "", "digests": { "md5": "d58b7eba7dc581b08280624554dd88b1", "sha256": "c74ccf842870e8a5c2f041a9641b6ce93d36b13834011b0258cfb549b7ac3c31" }, "downloads": -1, "filename": "FLiP-1.1.tar.gz", "has_sig": false, "md5_digest": "d58b7eba7dc581b08280624554dd88b1", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 85126, "upload_time": "2011-06-03T05:20:14", "url": "https://files.pythonhosted.org/packages/d6/21/56902f28a891c8879131595c98fe145516603c9f0025c686400bdb3395fc/FLiP-1.1.tar.gz" }, { "comment_text": "", "digests": { "md5": "d337feb5008a9df8f606aed40ed09f5d", "sha256": "d82a1e3d0df9c09a43e9382a310f940b267e23d2acf8c8d4fe699333c6f67dc7" }, "downloads": -1, "filename": "FLiP-1.1.zip", "has_sig": false, "md5_digest": "d337feb5008a9df8f606aed40ed09f5d", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 131202, "upload_time": "2011-06-03T05:26:10", "url": "https://files.pythonhosted.org/packages/79/dc/abc09fc7853f43f263145cfc87f093a45711c43c0d99acbb427b16c0bfad/FLiP-1.1.zip" } ], "1.2": [ { "comment_text": "", "digests": { "md5": "ae6012d4f79a670e05deba60e4107053", "sha256": "b2061c550ca0d51d759800788542dcfa73f2421d42b6ae458702ef3cc55c141c" }, "downloads": -1, "filename": "FLiP-1.2.tar.gz", "has_sig": false, "md5_digest": "ae6012d4f79a670e05deba60e4107053", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 93315, "upload_time": "2011-07-07T17:45:24", "url": "https://files.pythonhosted.org/packages/9f/1e/8048c9b55659576e745c830be73f1087f22a8df70b4a4768675bbe016bd8/FLiP-1.2.tar.gz" }, { "comment_text": "", "digests": { "md5": "ce850aea1af5ec2d4e670ad478dc54bf", "sha256": "f7d509d5dad2ff876182f7d9653ab30d078f544fece8db5cfd734ce04f97e671" }, "downloads": -1, "filename": "FLiP-1.2.zip", "has_sig": false, "md5_digest": "ce850aea1af5ec2d4e670ad478dc54bf", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 144150, "upload_time": "2011-07-07T17:45:27", "url": "https://files.pythonhosted.org/packages/db/4a/d97c4531c8ab44ea69a76798158079266432c946c26a59cddd939584dd89/FLiP-1.2.zip" } ] }, "urls": [ { "comment_text": "", "digests": { "md5": "ae6012d4f79a670e05deba60e4107053", "sha256": "b2061c550ca0d51d759800788542dcfa73f2421d42b6ae458702ef3cc55c141c" }, "downloads": -1, "filename": "FLiP-1.2.tar.gz", "has_sig": false, "md5_digest": "ae6012d4f79a670e05deba60e4107053", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 93315, "upload_time": "2011-07-07T17:45:24", "url": "https://files.pythonhosted.org/packages/9f/1e/8048c9b55659576e745c830be73f1087f22a8df70b4a4768675bbe016bd8/FLiP-1.2.tar.gz" }, { "comment_text": "", "digests": { "md5": "ce850aea1af5ec2d4e670ad478dc54bf", "sha256": "f7d509d5dad2ff876182f7d9653ab30d078f544fece8db5cfd734ce04f97e671" }, "downloads": -1, "filename": "FLiP-1.2.zip", "has_sig": false, "md5_digest": "ce850aea1af5ec2d4e670ad478dc54bf", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 144150, "upload_time": "2011-07-07T17:45:27", "url": "https://files.pythonhosted.org/packages/db/4a/d97c4531c8ab44ea69a76798158079266432c946c26a59cddd939584dd89/FLiP-1.2.zip" } ] }