JiscMail Logo
Email discussion lists for the UK Education and Research communities

Help for MATHEDU Archives


MATHEDU Archives

MATHEDU Archives


MATHEDU@JISCMAIL.AC.UK


View:

Message:

[

First

|

Previous

|

Next

|

Last

]

By Topic:

[

First

|

Previous

|

Next

|

Last

]

By Author:

[

First

|

Previous

|

Next

|

Last

]

Font:

Proportional Font

LISTSERV Archives

LISTSERV Archives

MATHEDU Home

MATHEDU Home

MATHEDU  July 2011

MATHEDU July 2011

Options

Subscribe or Unsubscribe

Subscribe or Unsubscribe

Log In

Log In

Get Password

Get Password

Subject:

CALL FOR PARTICIPATION - THedu'11 CTP components for educational software

From:

Pedro Quaresma <[log in to unmask]>

Reply-To:

Pedro Quaresma <[log in to unmask]>

Date:

Fri, 8 Jul 2011 12:12:32 +0100

Content-Type:

Text/Plain

Parts/Attachments:

Parts/Attachments

Text/Plain (99 lines)

                        CALL FOR PARTICIPATION
----------------------------------------------------------------------
                                THedu'11
                 CTP components for educational software
                 =======================================
                    (CTP -- Computer Theorem Proving)
                   http://www.uc.pt/en/congressos/thedu

                           Workshop at CADE-23,
           23nd International Conference on Automated Deduction
                 Wroclaw, Poland, July 31- August 5, 2011
                       http://cade23.ii.uni.wroc.pl/
----------------------------------------------------------------------

THedu'11 program: http://www.uc.pt/en/congressos/thedu/schedule
----------------
THeud'11 proceedings: http://www.uc.pt/en/congressos/thedu/proceedings
--------------------
THedu'11 Scope
--------------
This workshop intends to gather the research communities for Computer
Theorem proving (CTP), Automated Theorem Proving (ATP),  Interactive Theorem
Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic
Geometry Systems (DGS).
The goal of this union is to combine and focus systems of these areas and to
enhance existing educational software as well as studying the design of the
next generation of mechanised mathematics assistants (MMA). Elements for
next-generation MMA's include:

   * Declarative Languages for Problem Solution: education in applied
sciences and in engineering is mainly concerned with problems, which are
understood as operations on elementary objects to be transformed to an
object representing a problem solution. Preconditions and postconditions of
these operations can be used to describe the possible steps in the problem
space; thus, ATP-systems can be used to check if an operation sequence given
by the user does actually present a problem solution. Such "Problem Solution
Languages" encompass declarative proof languages like Isabelle/Isar or Coq's
Mathematical Proof Language, but also more specialized forms such as, for
example, geometric problem solution languages that express a proof argument
in Euclidean Geometry or languages for graph theory.

   * Consistent Mathematical Content Representation:  libraries of existing
ITP-Systems, in particular those following the LCF-prover paradigm, usually
provide logically coherent and human readable knowledge. In the leading
provers, mathematical knowledge is covered to an extent beyond most courses
in applied sciences. However, the potential of this mechanised knowledge for
education is clearly not yet recognised adequately: renewed pedagogy calls
for enquiry-based learning from concrete to abstract --- and the knowledge's
logical coherence supports such learning: for instance, the formula 2.pi
depends on the definition of reals and of multiplication; close to these
definitions are the laws like commutativity etc. Clearly, the complexity of
the knowledge's traceable interrelations poses a challenge to usability
design.

   * User-Guidance in Stepwise Problem Solving: Such guidance is
indispensable for independent learning, but costly to implement so far,
because so many special cases need to be coded by hand. However, CTP
technology makes automated generation of user-guidance reachable:
declarative languages as mentioned above, novel programming languages
combining computation and deduction, methods for automated construction with
ruler and compass from specifications, etc --- all these methods 'know how
to solve a problem'; so, using the methods' knowledge to generate
user-guidance mechanically is an appealing challenge for ATP and ITP, and
probably for compiler construction!

In principle, mathematical software can be conceived as models of
mathematics: The challenge addressed by this workshop is to provide
appealing models for MMAs which are interactive and which explain themselves
such that interested students can independently learn by inquiry and
experimentation.

Program Chairs
--------------
   Ralph-Johan Back, Abo University, Turku, Finland
   Pedro Quaresma, University of Coimbra, Portugal

Program Committee
   Francisco Botana, University of Vigo at Pontevedra, Spain
   Florian Haftmann, Munich University of Technology, Germany
   Predrag Janicic, University of Belgrade, Serbia
   Cezary Kaliszyk, University of Tsukuba, Japan
   Julien Narboux, University of Strasbourg, France
   Walther Neuper, Graz University of Technology, Austria
   Wolfgang Schreiner, Johannes Kepler University, Linz, Austria
   Laurent Théry, Sophia Antipolis, INRIA, France
   Makarius Wenzel, University Paris-Sud, France
   Burkhart Wolff, University Paris-Sud, France

-- 
  At\'e breve;\`A bient\^ot;See you later;Vidimo se;

Professor Auxiliar Pedro Quaresma
Departamento de Matem\'atica, Faculdade de Ci\^encias e Tecnologia
Universidade de Coimbra
P-3001-454 COIMBRA, PORTUGAL
correioE: [log in to unmask]
p\'agina: http://www.mat.uc.pt/~pedro/
telef: +351 239 791 137; fax: +351 239 832 568

Top of Message | Previous Page | Permalink

JiscMail Tools


RSS Feeds and Sharing


Advanced Options


Archives

February 2024
January 2024
September 2023
July 2023
June 2023
May 2023
April 2023
March 2023
January 2023
November 2022
October 2022
September 2022
July 2022
June 2022
May 2022
April 2022
March 2022
December 2021
November 2021
October 2021
September 2021
August 2021
July 2021
June 2021
April 2021
March 2021
February 2021
January 2021
November 2020
October 2020
August 2020
July 2020
June 2020
April 2020
March 2020
February 2020
January 2020
October 2019
September 2019
June 2019
February 2019
January 2019
December 2018
November 2018
September 2018
August 2018
July 2018
May 2018
April 2018
March 2018
February 2018
January 2018
November 2017
September 2017
June 2017
May 2017
March 2017
February 2017
November 2016
October 2016
September 2016
May 2016
April 2016
March 2016
April 2015
January 2015
December 2014
October 2014
May 2014
April 2014
March 2014
February 2014
January 2014
August 2013
July 2013
June 2013
May 2013
April 2013
March 2013
February 2013
December 2012
September 2012
June 2012
April 2012
February 2012
January 2012
December 2011
November 2011
September 2011
July 2011
June 2011
April 2011
March 2011
January 2011
December 2010
November 2010
October 2010
September 2010
August 2010
June 2010
May 2010
April 2010
March 2010
February 2010
January 2010
December 2009
November 2009
October 2009
September 2009
August 2009
July 2009
June 2009
May 2009
April 2009
March 2009
February 2009
January 2009
December 2008
November 2008
September 2008
August 2008
July 2008
June 2008
May 2008
April 2008
February 2008
December 2007
November 2007
October 2007
September 2007
August 2007
June 2007
May 2007
March 2007
February 2007
January 2007
December 2006
November 2006
September 2006
August 2006
July 2006
February 2006
January 2006
August 2005
July 2005
February 2005
December 2004
September 2004
July 2004
June 2004
May 2004
April 2004
January 2004
October 2003
July 2003
May 2003
April 2003
February 2003
December 2002
October 2002
September 2002
August 2002
July 2002


JiscMail is a Jisc service.

View our service policies at https://www.jiscmail.ac.uk/policyandsecurity/ and Jisc's privacy policy at https://www.jisc.ac.uk/website/privacy-notice

For help and support help@jisc.ac.uk

Secured by F-Secure Anti-Virus CataList Email List Search Powered by the LISTSERV Email List Manager