Re: [Hol-info] Two definitions of wellfoundedness

[Chun Tian (binghe)]

Hi,

ah... thanks, I didn’t see this theorem before.

—Chun

> Il giorno 11 set 2018, alle ore 10:08, Lorenz Leutgeb  ha 
> scritto:
> 
> Hi,
> 
> they are the same. Use the following theorem from prim_rec:
> 
> WF_IFF_WELLFOUNDED
> ⊢ ∀R. WF R ⇔ wellfounded R
> 
> Best,
> Lorenz
> 
> On Tue, 11 Sep 2018 at 17:59 Chun Tian (binghe)  > wrote:
> Hi,
> 
> in prim_recTheory, there’s a definition of ``wellfounded``:
> 
> [wellfounded_def]  Definition
> 
>   ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)
> 
> In relationTheory, there’s a definition of ``WF``:
> 
> [WF_DEF]  Definition
> 
>   ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b
> 
> are they essentially the same thing? (and if so, how to prove?)
> 
> —Chun
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Two definitions of wellfoundedness

[Lorenz Leutgeb via hol-info]

Hi,

they are the same. Use the following theorem from prim_rec:

WF_IFF_WELLFOUNDED
⊢ ∀R. WF R ⇔ wellfounded R

Best,
Lorenz

On Tue, 11 Sep 2018 at 17:59 Chun Tian (binghe) 
wrote:

> Hi,
>
> in prim_recTheory, there’s a definition of ``wellfounded``:
>
> [wellfounded_def]  Definition
>
>   ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)
>
> In relationTheory, there’s a definition of ``WF``:
>
> [WF_DEF]  Definition
>
>   ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b
>
> are they essentially the same thing? (and if so, how to prove?)
>
> —Chun
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CfP: Postproceedings ThEdu'18

[Walther Neuper]

   Open Call for Papers
**
   Postproceedings for ThEdu'18 by EPTCS
Theorem proving components for Educational software
http://www.uc.pt/en/congressos/thedu/thedu18
**
  Workshop ThEdu at FLoC
 Federated Logic Conference 2018
 http://www.floc2018.org/
**

THedu'18 Postproceedings:

  ThEdu's programme comprised seven contributions, presented also in the
  webpages. Now postproceedings are planned to collect the contributions
  upgraded to full papers. The contributions' topics are diverse
according   to ThEdu's scope, and this is a call open for everyone, also
those who   did not participate in the workshop. All papers will undergo
review   according to EPTCS standards.

THedu'18 Scope:

  Computer Theorem Proving is becoming a paradigm as well as a
  technological base for a new generation of educational software in
  science, technology, engineering and mathematics. The workshop brings
  together experts in automated deduction with experts in education in
  order to further clarify the shape of the new software generation and
  to discuss existing systems.

Topics of interest include:

 * methods of automated deduction applied to checking students' input;
 * methods of automated deduction applied to prove post-conditions
   for particular problem solutions;  * combinations of deduction and
computation enabling systems to
   propose next steps;  * automated provers specific for dynamic
geometry systems;
 * proof and proving in mathematics education.

Important Dates

 * 2nd call for papers:10 Sep 2018
 * Submission (full papers):   18 Nov 2018
 * Notification of acceptance: 17 Dec 2018
 * Revised papers due: 21 Jan 2019

Submission

  We welcome submission of papers presenting original unpublished work
  which is not been submitted for publication elsewhere.

  The authors should comply with the "instructions for authors", LaTeX
  style files and accept the "Non-exclusive license to distribute" of
  EPTCS:
Instructions for authors (http://info.eptcs.org/)
LaTeX style file and formatting instructions (http://style.eptcs.org/)
Copyright (http://copyright.eptcs.org/)

  Papers should be submitted via easychair,
  https://easychair.org/conferences/?conf=thedu18.

  In case the contributions finally do not reach the standards of EPTCS
  in number, there will be an alternative to publish as a techreport
  at CISUC https://www.cisuc.uc.pt/publications.

Program Committee
  Francisco Botana, University of Vigo at Pontevedra, Spain
  Roman Hašek, University of South Bohemia, Czech Republic
  Filip Maric, University of Belgrade, Serbia
  Walther Neuper, Graz University of Technology, Austria (co-chair)
  Pavel Pech, University of South Bohemia, Czech Republic
  Pedro Quaresma, University of Coimbra, Portugal (co-chair)
  Vanda Santos, CISUC, Portugal
  Wolfgang Schreiner, Johannes Kepler University, Austria
  Burkhart Wolff, University Paris-Sud, France



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Two definitions of wellfoundedness

[Chun Tian (binghe)]

Hi,

in prim_recTheory, there’s a definition of ``wellfounded``:

[wellfounded_def]  Definition

  ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)

In relationTheory, there’s a definition of ``WF``:

[WF_DEF]  Definition

  ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b

are they essentially the same thing? (and if so, how to prove?)

—Chun



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info