{"bugs":[],"categories":[{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"1b5853836e56a9b501dc27c4bbe3c999227db8be","committime":"2025-11-22T01:00:48","packageid":75732,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"c68a719fb2e69962d6fd4e9d5b706106dd7afd1f","committime":"2025-11-21T19:10:29","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: bump to 3.2.5"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"f1c14e3a77268023f69f56c7e1af6c35612e0fce","committime":"2025-11-21T19:05:32","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: drop old 3.0_pre008"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0b26f18b2cb2693f772e0f464b8306f4ac39a879","committime":"2024-02-19T21:03:52","packageid":75732,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/889682\nSigned-off-by: Maciej Barć ","commitid":"54392f0b0b647c60400cb91b124a103162bf2f2b","committime":"2024-02-19T20:34:06","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: fix build on musl"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"e7b55509858b599b2be09a27d3829055a8aeed34","committime":"2024-01-15T21:33:16","packageid":75732,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"49552e9fcd8f04cd3dde80b7935490ac3022d434","committime":"2024-01-15T20:19:45","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: bump to 3.0.03"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a2573336023d77abfd6ba29360a3237e56ab069c","committime":"2023-01-04T17:32:04","packageid":75732,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/889646\nSigned-off-by: Maciej Barć ","commitid":"e7417b60bbe948ef95486c7f3f139bc48351f2ff","committime":"2023-01-04T17:18:29","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: do not call ar\/ranlib directly"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"119c2528d84643fe3ec32014d28f20ec35e8f746","committime":"2023-01-04T03:46:57","packageid":75732,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"c6b0035d9cbec03b58b2af5f433e77a87b709822","committime":"2023-01-04T03:32:15","packageid":75732,"repoid":1,"summary":"sci-mathematics\/eprover: new package; add 3.0_pre008"}],"dependencies":[],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":882708,"firstseen":"2025-11-22T01:12:16.342739","license":"GPL-2+","moddate":"2026-03-22T20:20:57","packageid":75732,"repoid":1,"slot":"0","uses":["ho"],"version":"3.2.5"},{"archs":["~amd64","~x86"],"ebuildid":812008,"firstseen":"2024-01-15T21:51:54.911193","license":"GPL-2+","moddate":"2026-03-22T20:20:57","packageid":75732,"repoid":1,"slot":"0","uses":["ho"],"version":"3.0.03"}],"masks":[],"package":{"categoryid":317,"description":"Automated theorem prover for full first-order logic with equality","firstseen":"2023-01-04T04:03:07.398053","name":"eprover","packageid":75732,"summary":"E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms. If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it is of the form \"there exists an X with property P\"), more recent versions can also provide possible answers (values for X). Development of E started as part of the E-SETHEO project at TUM. The first public release was in in 1998, and the system has been continuously improved ever since. I believe that E now is one of the most powerful and friendly reasoning systems for first-order logic. The prover has successfully participated in many competitions."},"rdependencies":[],"repos":[{"branch":"master","lastcommit":"82366aa45a35f6900f43023917c2c86ccdbb00a3","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/eprover\/eprover\/","https:\/\/www.eprover.org\/"],"uses":[{"defaultflag":true,"description":"enable support for higher-order logic","isdefault":true,"packageid":75732,"use":"ho"}]}