Email Gateway (Aug 18 2022 at 10:07): Email Gateway (Aug 18 2022 at 10:07):From: Paqui Lucio <paqui.lucio@ehu.es>
The idea is to allow set expressions like "S1 Un {~A}" (or "S1 Un {~A} Un
S2") for representing
a set containing "~A" somewhere and, at the same time, naming the remaining
of the set by "S1". This would be
very useful to implement sequents calculi using de set.thy of Isabelle/HOL
to represent the antecedent (and the consequent in the symmetric case). I am
trying to do it, but I am a beginner Isabelle's user and parse_translations
are a bit hard for me.
Thanks,
Paqui
Paqui Lucio
Dpto de LSI
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20080-San Sebastián
SPAIN
e-mail: paqui.lucio@ehu.es
Tfn: (+34) (9)43 015049
Fax: (+34) (9)43 015590
Web: http://www.sc.ehu.es/paqui
Email Gateway (Aug 18 2022 at 10:08):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Is this much better than simply checking for set membership?
We tried to incorporate the Sequents.thy mechanism into HOL for our
DOVE environment and
found that all such rules needed to be augmented with a monotonicity
check. The trick. as
I recall, in Sequents.thy is to translate $F, A to something like F
(A) and allow higher-order
unification to solve the sequence membership problem. When you
actually try to model a semantics
for this, you find the need to check that the higher order function F
has the property of adding
A to the sequence membership. Thus you are really just moving the
semantic problem from one place
to another.
Email Gateway (Aug 18 2022 at 10:08):From: Paqui Lucio <paqui.lucio@ehu.es>
Is this much better than simply checking for set membership?
I think that it allows an easier and more natural way of reasoning
with sequent than the membersphip and subseteq checks, but
maybe I miss something about how using sets better than I do it.
We tried to incorporate the Sequents.thy mechanism into HOL
for our DOVE environment and found that all such rules needed
to be augmented with a monotonicity check. The trick. as I
recall, in Sequents.thy is to translate $F, A to something like F
(A) and allow higher-order
unification to solve the sequence membership problem. When
you actually try to model a semantics for this, you find the
need to check that the higher order function F has the
property of adding A to the sequence membership. Thus you are
really just moving the semantic problem from one place to another.
I see, thanks for the advice, I had imagine that semantics issues
should be more complicate than in the set case because the higher-order
unification. However, once you have proved the meta-logical properties
of your calculus (if possible) using a this more intrincate semantics,
the resulting calculus is, in my opinion, more suitable for users that
are accustomed to sequents.
Please, could you tell me how to have access to more information
(public .thy files and so on, if possible)
about your attempt for incorporating the Sequents.thy mechanism into HOL.
In particular, how do you solve the incompatibility between Pure and CPure.
Thanks in advance,
Paqui
On 02/02/2007, at 9:13 PM, Paqui Lucio wrote:
The idea is to allow set expressions like "S1 Un {~A}" (or "S1 Un
{~A} Un
S2") for representing
a set containing "~A" somewhere and, at the same time, naming the
remaining of the set by "S1". This would be very useful to
implement
sequents calculi using de set.thy of Isabelle/HOL to represent the
antecedent (and the consequent in the symmetric case). I am
trying to
do it, but I am a beginner Isabelle's user and
parse_translations are
a bit hard for me.
Email Gateway (Aug 18 2022 at 10:15):From: Paqui Lucio <paqui.lucio@ehu.es>
I wonder if there exists "a parser/print translation" for sets (from
HOL/set.thy) similar to the existing one for sequences in Sequents.thy. This
would allows us to work with sets in a more confortable way. ¿Does somebody
know some work on that?
Paqui
Paqui Lucio
Dpto de LSI
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20080-San Sebastián
SPAIN
e-mail: paqui.lucio@ehu.es
Tfn: (+34) (9)43 015049
Fax: (+34) (9)43 015590
Web: http://www.sc.ehu.es/paqui
Email Gateway (Aug 18 2022 at 10:15):From: Lawrence Paulson <lp15@cam.ac.uk>
This is an interesting idea, but it is non-trivial. The syntactic
treatment of sequents is designed to allow expressions like G, ~A, H
that represent a sequence of formulas containing ~A somewhere. It
relies on an encoding of associative unification in higher-order
unification. It allows sequent calculus rules to be written naturally.
It's not immediately clear to me how this could be added to the
current syntax for sets or what examples would benefit from it.
Larry Paulson
Last updated: May 03 2024 at 12:27 UTC