Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP AxiomaticCategoryTheory and smt_oracle

Email Gateway (Aug 25 2022 at 06:21):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi everyone,

There is one AFP entry AxiomaticCategoryTheory
(https://www.isa-afp.org/entries/AxiomaticCategoryTheory.html) that is
currently using smt_oracle. Nowadays, smt_oracle is against the rules of
submission. By a quick look over the linked arXiv entry, this usage is
also not explicitly mentioned.

However, it is now possible to make do without smt_oracle by simply
replacing the 3 failing smt calls by smt (verit). Would it make sense
do so?

Best,

Mathias

Email Gateway (Aug 26 2022 at 05:36):

From: Tobias Nipkow <nipkow@in.tum.de>
On 25/08/2022 08:20, Mathias Fleury wrote:

Hi everyone,

There is one AFP entry AxiomaticCategoryTheory
(https://www.isa-afp.org/entries/AxiomaticCategoryTheory.html) that is currently
using smt_oracle. Nowadays, smt_oracle is against the rules of submission. By a
quick look over the linked arXiv entry, this usage is also not explicitly mentioned.

However, it is now possible to make do without smt_oracle by simply replacing
the 3 failing smt calls by smt (verit). Would it make sense do so?

Absolutely, please go ahead.

Thanks
Tobias

Best,

Mathias

smime.p7s

Email Gateway (Aug 29 2022 at 06:04):

From: Mathias Fleury <mathias.fleury12@gmail.com>
For the record: done in ad3c436a878d
(https://isabelle-dev.sketis.net/rAFPad3c436a878d)

Email Gateway (Aug 29 2022 at 10:07):

From: Christoph Benzmueller <c.benzmueller@gmail.com>
Yes, thanks, C.

On Mon 29. Aug 2022 at 08:03 Mathias Fleury <mathias.fleury12@gmail.com>
wrote:

Univ.Prof. Dr. Christoph Benzmüller
Chair for AI Systems Engineering (AISE), Otto-Friedrich-Universität Bamberg
Prof. (apl.) at Dep. of Mathematics and Computer Science, FU Berlin
(http://christoph-benzmueller.de) <http://christoph-benzmueller.de/>

Last updated: Jan 04 2025 at 20:18 UTC