Re: [Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

2018-02-21 Thread Mario Xerxes Castelán Castro
Thanks.

On 21/02/18 11:57, Thomas Tuerk wrote:
> Hi,
> 
> the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
> description manual). AC normalisation would sort multiple occurrences of
> the same operant next to each other. Therefore these multiple
> occurrences can then be removed by providing 2 idempotency rewrite rules:
> 
> f x x = x
> 
> f x (f x y) = f x y
> 
> This provides a very high level simple way to do what you want, I believe.
> 
> If you want something lower level, more efficient with finer control,
> you could use "sort" from structure "AC_Sort". It provides a conversion
> that does what you want if instantiated properly. However, I never used
> it myself, so I don't have first hand experience with it.
> 
> There is also the structure "AC" from refute. However, I believe in
> contrast to "AC_Sort", there is no direct support for idempotency in "AC".
> 
> Cheers
> 
> Thomas



signature.asc
Description: OpenPGP digital signature
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


Re: [Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

2018-02-21 Thread Thomas Tuerk
Hi,

the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
description manual). AC normalisation would sort multiple occurrences of
the same operant next to each other. Therefore these multiple
occurrences can then be removed by providing 2 idempotency rewrite rules:

f x x = x

f x (f x y) = f x y

This provides a very high level simple way to do what you want, I believe.

If you want something lower level, more efficient with finer control,
you could use "sort" from structure "AC_Sort". It provides a conversion
that does what you want if instantiated properly. However, I never used
it myself, so I don't have first hand experience with it.

There is also the structure "AC" from refute. However, I believe in
contrast to "AC_Sort", there is no direct support for idempotency in "AC".

Cheers

Thomas


On 21.02.2018 18:34, Mario Xerxes Castelán Castro wrote:
> Hello.
>
> Is there an existing tactic for removing multiple appearances of an
> operand under an operator «f» that has the property «f x x = x» and is
> associative-commutative? For example, conjunction and disjunction.
>
> If not, I can write one for HOL4, but I do not want to duplicate
> existing work.
>
> Thanks.
>
>
>
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


[Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

2018-02-21 Thread Mario Xerxes Castelán Castro
Hello.

Is there an existing tactic for removing multiple appearances of an
operand under an operator «f» that has the property «f x x = x» and is
associative-commutative? For example, conjunction and disjunction.

If not, I can write one for HOL4, but I do not want to duplicate
existing work.

Thanks.



signature.asc
Description: OpenPGP digital signature
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


[Hol-info] WiL 2018: Women in Logic Workshop 2nd Call for Papers

2018-02-21 Thread Amy Felty
 Second Call for Papers
   WiL 2018: Second Women in Logic Workshop
  Oxford, UK
 8 July 2018
  https://sites.google.com/site/womeninlogic2018/welcome/

NEW
* Two invited speakers!
  (https://sites.google.com/site/womeninlogic2018/invited-speakers)
* New dates including extended submission deadline: 15 April 2018
* New format for paper submissions

Affiliated with the Thirty-Third Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS), 9-12 July 2018 (http://lics.siglog.org/lics18/)
and held as part of the Federated Logic Conference 2018 (FLoC), 6-19
July 2018 (http://www.floc2018.org/).

We are holding the second Women in Logic Workshop (WiL 2018) as a LICS
associated workshop this year. The workshop follows the pattern of
meetings such as Women in Machine Learning (WiML,
http://wimlworkshop.org/) or Women in Engineering (WIE,
http://www.ieee-ras.org/membership/women-in-engineering) that have
been taking place for quite a few years.

Women are chronically underrepresented in the LICS community;
consequently they sometimes feel both conspicuous and isolated, and
hence there is a risk that the under-representation is
self-perpetuating.

The workshop will provide an opportunity for women in the field to
increase awareness of one another and one another's work, to combat
the feeling of isolation. It will also provide an environment where
women can present to an audience comprised of mostly women,
replicating the experience that most men have at most LICS meetings,
and lowering the stress of the occasion; we hope that this will be
particularly attractive to early-career women.

Topics of interest of this workshop include but are not limited to the
usual Logic in Computer Science (LICS) topics. These are: automata
theory, automated deduction, categorical models and logics,
concurrency and distributed computation, constraint programming,
constructive mathematics, database theory, decision procedures,
description logics, domain theory, finite model theory, formal aspects
of program analysis, formal methods, foundations of computability,
higher-order logic, lambda and combinatory calculi, linear logic,
logic in artificial intelligence, logic programming, logical aspects
of bioinformatics, logical aspects of computational complexity,
logical aspects of quantum computation, logical frameworks, logics of
programs, modal and temporal logics, model checking, probabilistic
systems, process calculi, programming language semantics, proof
theory, real-time systems, reasoning about security and privacy,
rewriting, type systems and type theory, and verification.

INVITED SPEAKERS
* Brigitte Pientka (McGill University, Canada)
* Perdita Stevens (University of Edinburgh, UK)

IMPORTANT DATES
Paper submission deadline:  15 April 2018
Author notification:  15 May 2018
Contribution for Informal Proceedings:  31 May 2018

SUBMISSIONS
Contributions should be written in English and can be submitted in the
form of full papers (with a maximum of 10 pages), short papers (with a
maximum of 5 pages), or talk abstracts (1 page).

Formatting instructions: Papers and abstracts should be
prepared using the Easychair style
(https://easychair.org/publications/for_authors).

The submission should be in the form of a PDF file uploaded to the WiL
2018 Easychair page (https://easychair.org/conferences/?conf=wil2018)
before the submission deadline of 15 April 2018, anywhere on Earth.

PROCEEDINGS
We plan to publish an informal post conference volume at ENTCS or
other equally visible outlet.

SCIENTIFIC AND ORGANIZING COMMITTEE
* Valeria de Paiva (Co-Chair, Nuance Communications, USA)
* Adriana Compagnoni (Stevens Institute of Technology, USA)
* Amy Felty (Co-Chair, University of Ottawa, Canada)
* Anna Ingolfsdottir (Reykjavik University, Iceland)
* Sara Kalvala (University of Warwick, UK)
* Ursula Martin (University of Oxford, UK)
* Valeria Vignudelli (Ecole Normale Supérieure de Lyon, France)

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info