Email Gateway (Aug 22 2022 at 10:06): Email Gateway (Aug 22 2022 at 10:06):From: Mandy Martin <tesleft@hotmail.com>
Hi ,
how to classify logic rules that belong to an axiom system?
how to know that which rules together form a axiom system?
Regards,
Martin Lee
Email Gateway (Aug 22 2022 at 10:06):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,
what do you mean by the classification of logic rules? The best would be to cite some paper or book you got this idea from.
To your second question: you can define any axiom system you want but what property do you want to achieve? Being free of contradictions? Please detail this.
Email Gateway (Aug 22 2022 at 10:07):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,
what do you want to model by your axiom system? Do you want to create a logical framework for general mathematics or some concrete axiom system for geometry or number theory?
And, what does this have to do with the Isabelle theorem prover? If you are at the theoretical beginning of your research you might better ask on
http://math.stackexchange.com/questions/tagged/logic
Cheers
Email Gateway (Aug 22 2022 at 10:08):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,
what do you mean by "script"? An Isabelle script? If you want to pose beginner questions about writing Isabelle scripts the place is
http://stackoverflow.com/questions/tagged/isabelle
But even there you cannot expect that others will write full proof scripts for your problems.
Could you tell us how did you arrive to Isabelle? Do you attend a course on verification somewhere or is it purely a personal interest?
Email Gateway (Aug 22 2022 at 10:08):From: Makarius <makarius@sketis.net>
BTW, the terminology of "proof scripts" was abandoned for Isabelle/Isar in
1998 or so, and replaced by "proof texts" or "proof documents".
Since Proof General with its "scripting" mode was still used until last
year, there was a remaining confusion about that. In Isabelle2015,
support for Proof General and the TTY command-line no longer exists, and
it is all about interactive proof document editing in PIDE.
Makarius
Email Gateway (Aug 22 2022 at 10:09):From: Mandy Martin <tesleft@hotmail.com>
Hi Buday,
i can validate whether it is a correct rule by more one in output cover less one in two input and filter all possible rules from all combination of equations but i do not know the steps about how to form an axiom system. for example, how to choose which rules, which book teaching this and any web resources teaching this?any properties list show all existing properties?actually i do not know which property it output. i just want to filter and form all axioms system including unknown axioms system and research the usage of them.
i am not sure whether a, b -> c # two logic input and 1 logic output is called 3 termed syllogism. if so, i am using this kind of rules.
Regards,
Martin Lee
Last updated: Apr 25 2024 at 08:20 UTC