{"payload":{"pageCount":2,"repositories":[{"type":"Public","name":"theoremprover-museum.github.io","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":16,"starsCount":51,"forksCount":7,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-11T10:59:06.365Z"}},{"type":"Public","name":"fellowship","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"OCaml","color":"#ef7a08"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T19:11:59.052Z"}},{"type":"Public","name":"minlog","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-06T18:59:01.368Z"}},{"type":"Public","name":"larch","owner":"theoremprover-museum","isFork":false,"description":"The Larch Theorem Prover from MIT","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-03T11:38:38.254Z"}},{"type":"Public","name":"Ehdm","owner":"theoremprover-museum","isFork":false,"description":"The Ehdm theorem prover developed at SRI in the 80s. ","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-06-22T11:59:28.766Z"}},{"type":"Public","name":"egal","owner":"theoremprover-museum","isFork":false,"description":"Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory","allTopics":["theorem-proving","verification","proof-assistant","set-theory","higher-order-logic","theorem-prover"],"primaryLanguage":{"name":"OCaml","color":"#ef7a08"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-07-15T16:39:06.953Z"}},{"type":"Public","name":"SEQUEL","owner":"theoremprover-museum","isFork":false,"description":"Mark Tarver's SEQUEL system versions 7.0 and 5.3","allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-07-06T11:40:11.329Z"}},{"type":"Public archive","name":"oleg","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Standard ML","color":"#dc566d"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-05-02T12:00:20.562Z"}},{"type":"Public","name":"doc","owner":"theoremprover-museum","isFork":false,"description":"Documentation about the Theorem Prover Museum","allTopics":[],"primaryLanguage":{"name":"TeX","color":"#3D6117"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-06-11T06:18:47.969Z"}},{"type":"Public","name":"muscadet","owner":"theoremprover-museum","isFork":false,"description":"The Muscadet Theorem Prover is a knowledge-based system. Based on natural deduction, it uses methods which resemble those used by humans, implemented in one or several bases of facts. The output is an easily readable proof.","allTopics":[],"primaryLanguage":{"name":"Prolog","color":"#74283c"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":1,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-12-07T17:23:21.426Z"}},{"type":"Public","name":"Peers-mcd","owner":"theoremprover-museum","isFork":false,"description":"the Peers-mcd theorem provers","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-09-28T17:59:50.217Z"}},{"type":"Public","name":"Peers","owner":"theoremprover-museum","isFork":false,"description":"The Peers Theorem Prover","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-09-18T15:43:57.527Z"}},{"type":"Public","name":"Aquarius","owner":"theoremprover-museum","isFork":false,"description":"The Aquarius Theorem Prover","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-09-18T15:17:28.638Z"}},{"type":"Public","name":"LEGO","owner":"theoremprover-museum","isFork":false,"description":"the source archive for LEGO: an interactive proof development system for various type theories","allTopics":[],"primaryLanguage":{"name":"Lex","color":"#DBCA00"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-21T05:23:25.757Z"}},{"type":"Public","name":"isabelle","owner":"theoremprover-museum","isFork":false,"description":"Archival Versions of the Isabelle Theorem Prover","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-20T06:04:58.006Z"}},{"type":"Public","name":"EQP","owner":"theoremprover-museum","isFork":false,"description":" EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search. ","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":5,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-20T05:59:43.150Z"}},{"type":"Public","name":"PLTP","owner":"theoremprover-museum","isFork":false,"description":"The Edinburgh Pure Lisp Theorem Prover (Boyer/Moore)","allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-19T11:46:40.412Z"}},{"type":"Public","name":"ClassInt","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-19T11:09:28.081Z"}},{"type":"Public","name":"RDL","owner":"theoremprover-museum","isFork":false,"description":" Rewrite and Decision Procedure Laboratory","allTopics":[],"primaryLanguage":{"name":"Prolog","color":"#74283c"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-06-19T10:49:17.031Z"}},{"type":"Public","name":"prover9","owner":"theoremprover-museum","isFork":false,"description":"Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":16,"forksCount":3,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2018-05-04T16:44:01.292Z"}},{"type":"Public","name":"logic-theorist","owner":"theoremprover-museum","isFork":false,"description":"The sources of the first theorem prover.","allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":1,"starsCount":55,"forksCount":6,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-09-02T16:10:01.067Z"}},{"type":"Public","name":"SETHEO","owner":"theoremprover-museum","isFork":false,"description":"The SETHEO theorem prover (C version)","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-06-27T12:39:20.069Z"}},{"type":"Public","name":"ProCom","owner":"theoremprover-museum","isFork":false,"description":"A theorem prover based on the PTTP paradigm.","allTopics":[],"primaryLanguage":{"name":"Prolog","color":"#74283c"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-06-26T06:33:48.361Z"}},{"type":"Public","name":"scunac","owner":"theoremprover-museum","isFork":false,"description":"a proof checker and interactive theorem prover for dependently typed set theory","allTopics":[],"primaryLanguage":{"name":"Common Lisp","color":"#3fb68b"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-05-16T16:34:00.533Z"}},{"type":"Public","name":"SNARK","owner":"theoremprover-museum","isFork":false,"description":"SNARK - SRI's New Automated Reasoning Kit","allTopics":[],"primaryLanguage":{"name":"Common Lisp","color":"#3fb68b"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-04-07T05:55:10.076Z"}},{"type":"Public","name":"discount","owner":"theoremprover-museum","isFork":false,"description":"the discount theorem prover","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-04-07T04:43:23.330Z"}},{"type":"Public","name":"lambdaclam","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"AMPL","color":"#E6EFBB"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-04-04T14:03:15.870Z"}},{"type":"Public","name":"HOL90","owner":"theoremprover-museum","isFork":false,"description":"The source of hte HOL90 Theorem prover. ","allTopics":[],"primaryLanguage":{"name":"Standard ML","color":"#dc566d"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-03-28T09:44:14.925Z"}},{"type":"Public","name":"OSHL","owner":"theoremprover-museum","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2017-01-09T14:19:37.265Z"}},{"type":"Public","name":"clam3","owner":"theoremprover-museum","isFork":false,"description":"Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.","allTopics":[],"primaryLanguage":{"name":"Prolog","color":"#74283c"},"pullRequestCount":0,"issueCount":0,"starsCount":6,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2016-12-30T18:50:53.052Z"}}],"repositoryCount":42,"userInfo":null,"searchable":true,"definitions":[],"typeFilters":[{"id":"all","text":"All"},{"id":"public","text":"Public"},{"id":"source","text":"Sources"},{"id":"fork","text":"Forks"},{"id":"archived","text":"Archived"},{"id":"template","text":"Templates"}],"compactMode":false},"title":"theoremprover-museum repositories"}