{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":15494792,"defaultBranch":"master","name":"tpg","ownerLogin":"wo","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2013-12-28T15:54:44.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/145954?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1388246158.0","currentOid":""},"activityList":{"items":[{"before":"64f7db9c22f13387a842265d713d1991861353ca","after":"31b11b603f978c51d56684f106439edb6e850262","ref":"refs/heads/master","pushedAt":"2023-07-15T15:36:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wo","name":"Wolfgang Schwarz","path":"/wo","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145954?s=80&v=4"},"commit":{"message":"slightly tweak proof search to speed up some proofs\n\nThe previous commit 64f7db9 caused a strong slowdown of some proofs,\nespecially pel51. This tweak brings the proof time down from 48s to 28s.\nAs usual with this kind of change, the overall effect is mixed, but\nseems to be positive.","shortMessageHtmlLink":"slightly tweak proof search to speed up some proofs"}},{"before":"e68983733c4a6e49eba58a9004a6d8ac32956662","after":"64f7db9c22f13387a842265d713d1991861353ca","ref":"refs/heads/master","pushedAt":"2023-07-15T14:03:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wo","name":"Wolfgang Schwarz","path":"/wo","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145954?s=80&v=4"},"commit":{"message":"fix pruneAlternatives\n\nWhen checking for redundant alternatives among prover.alternatives, I\nused to compare different trees by checking if each open branch on one\nextends some open branch on another. This is problematic if the trees\ncontain a disjunction p v p (with the same disjunct on both sides). Any\nbranch that develops the left disjunct on tree1 then extends the\nundeveloped right-hand branch on tree2, even if tree1 and tree2\notherwise explore very different strategies.\n\nThe present change helps with issue #23 on github, but it causes a\nregression for Pelletier's problem 51, which was previously provable in\n2508 steps and now appears to become unprovable in any reasonable time.\n(Problems 49 and 52 also perform much worse.)","shortMessageHtmlLink":"fix pruneAlternatives"}},{"before":"deae847054d70583d9ce83e39def1a807d565c67","after":"e68983733c4a6e49eba58a9004a6d8ac32956662","ref":"refs/heads/master","pushedAt":"2023-07-14T12:23:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wo","name":"Wolfgang Schwarz","path":"/wo","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145954?s=80&v=4"},"commit":{"message":"add better logging options\n\nYou can now limit the debugging output with debug=prover,\ndebug=modelfinder, etc., as well as debug=trace.","shortMessageHtmlLink":"add better logging options"}},{"before":"938f2449e9ab49029d2a64afc9b18bed3ca336a9","after":"deae847054d70583d9ce83e39def1a807d565c67","ref":"refs/heads/master","pushedAt":"2023-04-28T19:43:53.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"wo","name":"Wolfgang Schwarz","path":"/wo","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145954?s=80&v=4"},"commit":{"message":"fix order of [] and (Ax) processing\n\nWhen expanding □∀x□∀y(□Fx∨□Gy)→(□∀x□Fx∨□∀x□Gx) in S4, we have a lot of\noptions of wR* for the outermost box in the antecedent; only one of them\nleads to a closed tree. Previously, the prover was very slow at\niterating through the options because the modalGamma function put itself\nat the very end of the todo queue after each application. Now we\nimmediately expand [] formulas with all available options.","shortMessageHtmlLink":"fix order of [] and (Ax) processing"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAADVjZbNQA","startCursor":null,"endCursor":null}},"title":"Activity · wo/tpg"}