Re: tactic works only once

------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:

Build for Windows Store.

http://p.sf.net/sfu/windows-dev2dev

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: tactic works only once

------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:

Build for Windows Store.

http://p.sf.net/sfu/windows-dev2dev

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

tactic works only once

------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:

Build for Windows Store.

http://p.sf.net/sfu/windows-dev2dev

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

CfP for Math. in Computer Science Special Issue on 'Enabling Domain Experts to use Formalised Reasoning' (deadline 31 Oct)

     Call for Papers for a Special Issue of MATHEMATICS IN COMPUTER SCIENCE

              ENABLING DOMAIN EXPERTS TO USE FORMALISED REASONING
       http://www.cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

           Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat

We invite high-quality original research papers to a special issue of
the Birkhäuser/Springer journal Mathematics in Computer Science on the
use of systems based on a formal, explicit, machine-verifiable
representation of knowledge in application domains such as economics,
engineering, health care, education. Examples include:

* problems from application domains, which could benefit from better
  verification and knowledge management facilities, and

* knowledge management and verification tools, which domain experts
  can use without a computer science background. (Read more about our
  topics of interest)

For further examples, please see the Symposium on Enabling Domain
Experts to use Formalised Reasoning
(http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/)
held at the annual convention of the AISB (Society for the Study of
Artificial Intelligence and Simulation of Behaviour) in April 2013.

    Submission: 31 October 2013
    Notification: 15 December 2013
    Revised version due: 15 January 2014
    Final version due: 15 February 2014
    Publication (expected): April 2014

Topics of interest include but are not limited to:

* for domain experts: what problems in application domains could
  benefit from better verification and knowledge management
  facilities? Possible fields include:

  - Example 1 (economics): auctions, value-at-risk models, trading
    algorithms, market design

  - Example 2 (engineering): system interoperability, manufacturing
    processes, product classification

* for computer scientists: how to provide the right knowledge
  management and verification tools to domain experts without a
  computer science background?

  -  wikis and blogs for informal, semantic, semiformal, and formal
     mathematical knowledge;
  -  general techniques and tools for online collaborative mathematics;
  -  tools for collaboratively producing, presenting, publishing, and
     interacting with online mathematics;
  -  automation and human-computer interaction aspects of mathematical
wikis;
  -  ontologies and knowledge bases designed to support knowledge
     management and verification in application domains;
  -  practical experiences, usability aspects, feasibility studies;
  -  evaluation of existing tools and experiments;
  -  requirements, user scenarios and goals.

Submissions should be approximately 20 pages long, should follow
publishers' instructions and should be submitted via EasyChair.

Potential contributors may contact the guest editors
(doformmcs2014 <at> easychair.org) to discuss the suitability of topics and
papers.

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Early registration deadline 23 June; http://cicm-conference.org/2013/
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 1 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 5 July; http://www.iaoa.org/womo/2013.html

------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:

Build for Windows Store.

http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Book announcement: ALAN TURING - His Work and Impact

************************************************************************
New book announcement: "ALAN TURING: His Work and Impact" 
- edited by S. Barry Cooper and Jan van Leeuwen
http://store.elsevier.com/product.jsp?isbn=9780123869807

"The fact remains that everyone who taps at a keyboard, opening a 
spreadsheet or a word-processing program, is working on an incarnation of 
a Turing machine." -TIME Magazine

In one accessible volume, this book presents the most significant original 
works from the 4-volume set of A.M Turing's collected works, along with 
key commentary from over 70 great scholarly leaders in the field, 
providing interested readers with unique insight into the context and 
significance of Turing's impact on mathematics, computing, computer 
science, informatics, morphogenesis, philosophy and the wider scientific 
world.

This remarkable volume is an essential addition to any library, private or 
institutional.

* See below for an engrossing article from Elsevier Connect on the book 
and its genesis:

- New book spotlights Alan Turing, Nazi code-breaker and 'father of 
computer science'
- Turing's work has influenced scholars in many fields; Editor Barry 
Cooper talks about compiling their commentary along with Turing's writing

http://elsevierconnect.com/new-book-spotlights-alan-turing-nazi-code-breaker-and-father-of-computer-science/
http://bit.ly/11qVF66

************************************************************************

------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:

Build for Windows Store.

http://p.sf.net/sfu/windows-dev2dev

CFP Synasc 2013, Timisoara, Romania

[Please post - apologies for multiple copies.]

Call for Papers
---------------

                       SYNASC 2013

              15th International Symposium on
   Symbolic and Numeric Algorithms for Scientific Computing
         September 23-26, 2013, Timisoara, Romania
                   http://www.synasc.ro/

Aim
---

SYNASC aims to stimulate the interaction between the two 
scientific communities of symbolic and numeric computing 
and to exhibit interesting applications of the areas both 
in theory and in practice. The choice of the topic is motivated 
by the belief of the organizers that the dialogue between 
the two communities is very necessary for accelerating the 
progress in making the computer a truly intelligent aid for 
mathematicians and engineers.

Important Dates
---------------

23 June 2013 (EXTENDED) :  Abstract submission   
30 June 2013 (EXTENDED) :  Paper submission  
04 August 2013          :  Notification of acceptance
01 September 2013       :  Registration
08 September 2013       :  Revised papers according to the reviews
23-26 September 2013    :  Symposium
30 November 2013        :  Final papers for post-proceedings

Tracks
------

    * Symbolic Computation
        + computer algebra
        + symbolic techniques applied to numerics
        + hybrid symbolic and numeric algorithms
        + numerics and symbolics for geometry
        + programming with constraints, narrowing

    * Logic and Programming
        + automatic reasoning
        + formal system verification
        + formal verification and synthesis
        + software quality assessment
        + static analysis
        + timing analysis

    * Artificial Intelligence
        + methods for hard computational problems
        + intelligent systems for scientific computing
        + agent-based complex systems modeling and development
        + scientific knowledge management
        + computational intelligence 
        + machine learning 
        + recommender and expert systems for scientific computing
        + data mining and web mining
        + natural language processing  
        + uncertain reasoning in scientific computing       
        + intelligent hybrid systems

    * Numerical Computing
        + iterative approximation of fixed points
        + solving systems of nonlinear equations
        + numerical and symbolic algorithms for differential equations
        + numerical and symbolic algorithms for optimization
        + parallel algorithms for numerical computing
        + scientific visualization and image processing

    * Distributed Computing
        + parallel and distributed algorithms for clouds, GPUs, HPC, P2P systems, 

autonomous systems. Work should focus on scheduling, scaling, load balancing, networks, 

fault-tolerance, gossip algorithms, energy saving
        + applications for parallel and distributed systems, including work on cross 

disciplinary (scientific) applications for grids/clouds, web applications, workflow 

platforms, network measurement tools, programming environments
        + architectures for parallel and distributed systems, including self-managing and 

autonomous systems, negotiation protocols, HPC on clouds, GPU processing, PaaS for 

(inter)cloud, brokering platforms, mobile computing
        + modelling of parallel and distributed systems including models on resources and 

networks, semantic representation, negotiation, social networks, trace management, 

simulators
        + any other topic deemed relevant to the field

    * Advances in the Theory of Computing
       + Data structures and algorithms
       + Combinatorial Optimization
       + Formal languages and Combinatorics on Words
       + Graph-theoretic and Combinatorial methods in Computer Science
       + Algorithmic paradigms, including distributed, online, 
         approximation, probabilistic, game-theoretic algorithms
       + Computational Complexity Theory, including structural complexity, 
         boolean complexity, communication complexity, average-case complexity, 
         derandomization and property testing
       + Logical approaches to complexity, including finite model theory
       + Algorithmic and computational learning theory
       + Aspects of computability theory, including computability in 
         analysis and algorithmic information theory
       + Proof complexity
       + Computational social choice and game theory
       + New computational paradigms: CNN computing, quantum, 
         holographic and other non-standard approaches to Computability
       + Randomized methods, random graphs, threshold phenomena and 
         typical-case complexity
       + Automata theory and other formal models, particularly in
         relation to formal verification methods such as model 
         checking and runtime verification
       + Applications of theory, including wireless and sensor networks, 
         computational biology and computational economics
       + Experimental algorithmics

Workshops
---------
    * Workshop on Agents for Complex Systems (ACSys) 
           http://www.synasc.ro/workshops/acsys-2013/
    * Workshop of HPC for scientific problems (HPCSP)
           http://host.hpc.uvt.ro/events/hpcsp/ 
    * Workshop on Iterative Approximation of Fixed Points (IAFP)
           http://www.synasc.ro/workshops/iafp-2013/
    * Workshop on Management of Resources and Services in Cloud and Sky Computing (MICAS)
           http://amicas.hpc.uvt.ro/micas-2013/
    * Workshop on Natural Computing and Applications (NCA)
           http://www.synasc.ro/workshops/nca-2013/

    Workshops deadlines:  please visit each workshop webpage

Tutorials
---------

    * Tutorial HPC http://host.hpc.uvt.ro/hpcs#HPC-Tutorial
    * Tutorial Multi-Cloud http://amicas.hpc.uvt.ro/micas-2013#MultiCloud-Tutorial

     
Publication
-----------
Research papers that are accepted and presented at the 
symposium will be collected as post-proceedings published 
by Conference Publishing Service (CPS) (indexed in ISI Web 
of Science, DBLP, SCOPUS).

Invited Speakers 
----------------
    * Ivona Brandic,     Vienna University of Technology, Austria
    * Gabriel Ciobanu,   Romanian Academy, Institute of Computer Science, Iasi, Romania
    * Leonardo de Moura, Microsoft Research, USA
    * Grigore Rosu,      University of Illinois at Urbana-Champaign, USA
    * Dan A. Simovici,   University of Massachusetts Boston, USA

   
Honorary Chairs
---------------
    * Bruno Buchberger, Johannes Kepler University, Austria
    * Stefan Maruster, West University of Timisoara, Romania

Steering Committee
------------------
    * Tetsuo Ida, University of Tsukuba, Japan
    * Tudor Jebelean, Johannes Kepler University, Austria
    * Viorel Negru, West University of Timisoara, Romania
    * Dana Petcu, West University of Timisoara, Romania
    * Stephen Watt, University of Western Ontario, Canada
    * Daniela Zaharie, West University of Timisoara, Romania

General Chair
-------------
    * Viorel Negru, West University of Timisoara, Romania

Program Chair
-------------
    * Nikolaj Bjorner, Microsoft Research, US

Track Chairs
------------
    * Symbolic Computation
        + Tetsuo Ida, University of Tsukuba, Japan
        + Stephen Watt, University of Western Ontario, Canada

    * Logic and Programming
        + Tudor Jebelean, Johannes Kepler University, Austria
        + Laura Kovacs, Chalmers University of Technology, Sweden

    * Artificial Intelligence
        + Andrei Petrovski, Robert Gordon University, UK        
        + Daniela Zaharie, West University of Timisoara, Romania

    * Numerical Computing
        + Yonghong Yao, Tianjin Polytechnic University, China
        + Ioan A. Rus, "Babes-Bolyai" University of Cluj-Napoca, Romania

    * Distributed Computing
        + Marc Frincu, West University of Timisoara, Romania
        + Karoly Bosa, Johannes Kepler University, Austria

    * Advances in the Theory of Computing
        + Mircea Marin, West University of Timisoara, Romania
        + Gabriel Istrate, Research Institute e-Austria Timisoara, Romania

Special sessions and workshops chair
------------------------------------
    * Dana Petcu, West University of Timisoara, Romania

Tutorial chair
--------------
    * Adrian Craciun, West University of Timisoara, Romania

Proceedings Chairs
------------------
    * Nikolaj Bjorner, Microsoft Research, US
    * Daniela Zaharie, West University of Timisoara, Romania

Local Committee Chairs
----------------------
    * Isabela Dramnesc, West University of Timisoara, Romania
    * Silviu Panica, Institute e-Austria Timisoara, Romania

Submission
-----------

Submissions of research papers are invited. The papers must contain 
original research results not submitted and not published elsewhere. 

The submission process consists of two steps.  

    * In the first step the authors are invited to express their 
      intention to participate at the conference by submitting a 
      short abstract (1/2 page, at maximum) where it is clearly 
      stated the main contribution(s) of the paper.

    * In the second step the authors should submit the full paper
      (up to 8 pages in the two-columns IEEE conference style).

Both the abstract and the full paper should be submitted electronically 
through http://www.easychair.org/conferences/?conf=synasc2013 (for the main tracks)
and through http://www.easychair.org/conferences/?conf=synasc2013workshops (for the 

workshops).

Proposals are also invited for:

    * special sessions

Special sessions
----------------

Proposals are invited for special sessions on any topic relevant to the 
conference. Special sessions are intended to stimulate in-depth  
discussions in special areas and they are fully integrated into the 
main conference. The research papers and the informal presentations 
submitted and accepted for the special sessions follow the same rules 
as the papers submitted to the regular sessions. It is expected that 
the organizers of the special sessions appoint their own chair and 
program committee, which will be integrated in the conference program 
committee and will be supervised by the conference programme chair 
and by the general chair.

-----------
SYNASC 2013
West University of Timisoara
Department of Computer Science
Bd. V. Parvan 4, 300223 Timisoara, Romania
tel: + (40) 256 592155, +(40) 256 592195
fax: + (40) 256 592316, +(40) 256 592380
e-mail: synasc13 <at> synasc.ro

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j

Hol Light packages for Debian (and Ubuntu)

Hi,

as you may have noticed, Debian contains now a package for Hol
Light (http://packages.debian.org/stable/hol-light). Debian
stable contains svn revision 146 from 2012-06-02 and testing
currently contains revision 162 from 2013-05-11. I will update
the package in testing about every few month, so that it will be
reasonable up-to-date. As Debian version I use the date of the
svn commit of the respective version.

The package is also available on Ubuntu
(https://launchpad.net/ubuntu/+source/hol-light) and can probably
be installed on many Debian derivatives. 

After package installation you will find some information on
related packages and about using checkpoints in
/usr/share/doc/hol-light/README.Debian .

If you have questions or problems with the package please submit
a Debian bug or contact me directly by email.

On a different topic: For about a year, support for Hol Light in
Proof General and for proof-tree visualization
(http://askra.de/software/prooftree/) is close before the first
public announcement without making any progress. Many things work
already, it just needs a Hol Light + Emacs user to fix the
remaining issues. 

Bye,

Hendrik

PS. Please CC me on replies, I have not subscribed hol-info.

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j

Call for Participation CICM 2013 8-12 July 2013, Registration deadline 23rd June 2013

     CICM 2013 - Conferences on Intelligent Computer Mathematics
         July 8-12, 2013 at University of Bath, Bath, UK

            http://cicm-conference.org/2013/cicm.php

                     Call for participation 

                Registration deadline: 23 June 2013
-----------------------------------------------------------------------
Invited talks will be given by:

- Patrick Ion, Mathematical Reviews, American Mathematical Society, USA
- Assia Mahboubi, École Polytechnique and INRIA/Microsoft Research
  Joint Centre, France
- Ursula Martin, Queen Mary, University of London, UK

Co-Located Workshops:
- MathUI'13: Mathematical User Interfaces
- OpenMath Workshop 2013
- PLMMS'13: Programming Languages for Mechanized Mathematics Systems
- THedu'13: TP Components for Educational Software

The  global programme  of the  conference, tracks,  and  workshops are
available via:

http://cicm-conference.org/2013/cicm.php?event=&menu=detailed-programme

Accepted Papers:

- Pedro  Quaresma, Vanda  Santos  and Seifeddine  Bouallegue. The  Web
  Geometry Laboratory Project
- Russell  Bradford, James  H.  Davenport, Matthew  England and  David
  Wilson.  Optimising Problem  Formulation  for Cylindrical  Algebraic
  Decomposition
- Matthew  England, Russell  Bradford,  James H.  Davenport and  David
  Wilson. Understanding branch cuts of expressions
- Christoph Lange, Colin Rowat and Manfred Kerber. The ForMaRE Project
  - Formal Mathematical Reasoning in Economics
- Cezary Kaliszyk and Josef Urban. Automated Reasoning Service for HOL
  Light Corpora
- Jónathan Heras and  Ekaterina Komendantskaya. ML4PG: proof-mining in
  Coq
- Jónathan  Heras,  Gadea Mata,  Ana  Romero,  Julio  Rubio and  Rubén
  Sáenz.  Verifying  a  platform  for digital  imaging:  a  multi-tool
  strategy
- Dmitry  Chebukov, Alexandr  Izaak, Olga  Misurina, Yury  Pupyrev and
  Alexey Zhizhchenko. Math-Net.Ru as  a Digital Archive of the Russian
  Mathematical Knowledge
- Chau  Do  and Eric  Pauwels.  Using  MathML  to Represent  Units  of
  Measurement for Improved Ontology Alignment
- Miguel A. Abanades and Francisco Botana. A dynamic symbolic geometry
  environment for the computation of geometric loci and envelopes
- Shahab  Kamali and  Frank  Tompa. Structural  Similarity Search  For
  Mathematics Retrieval
- Rui  Hu   and  Stephen  Watt.  Determining   Points  on  Handwritten
  Mathematical Symbols
- Rein Prank. Software for  evaluating relevance of steps in algebraic
  transformations
- Eno  Tonisson. When  Students  Compare Their  Own  Answers with  the
  Answers of a Computer Algebra System
- Carst   Tankink,   Cezary   Kaliszyk,   Josef   Urban   and   Herman
  Geuvers. Formal Mathematics on Display: A Wiki for Flyspeck
- Michael Kohlhase, Felix Mance  and Florian Rabe. A Universal Machine
  for Biform Theory Graphs
- Florian Rabe. The MMT API: A Generic MKM System
- William  Farmer.  The  Formalization  of  Syntax-Based  Mathematical
  Algorithms Using Quotation and Evaluation
- Paul Libbrecht. Escaping the Trap of too Precise Topic Queries
- Bruno  Barras, Hugo  Herbelin, Lourdes  Del Carmen  González Huesca,
  Yann  Régis-Gianas,  Enrico  Tassi,  Makarius  Wenzel  and  Burkhart
  Wolff. Pervasive Parallelism in Highly-Trustable Interactive Theorem
  Proving Systems
- Christoph Lange,  Marco Caminati, Manfred  Kerber, Till Mossakowski,
  Colin Rowat, Makarius Wenzel and Wolfgang Windsteiger. A Qualitative
  Comparison  of the  Suitability of  Four Theorem  Provers  for Basic
  Auction Theory
- Deyan Ginev and Bruce Miller. LaTeXML 2012 - A Year of LaTeXML
- Xavier  Allamigeon,  Stéphane Gaubert,  Victor  Magron and  Benjamin
  Werner.  Certification  of   Bounds  of  Non-linear  Functions:  the
  Templates Method
- Bruce Miller. 3 Years of DLMF on the Web; Math & Search
- Minh-Quoc Nghiem,  Giovanni Yoko  Kristianto, Goran Topic  and Akiko
  Aizawa.  A  hybrid  approach   for  semantic  enrichment  of  MathML
  mathematical expressions
- Steven Obua,  Mark Adams and  David Aspinall. Capturing  Hiproofs in
  HOL Light
- Ulf Schöneberg  and Wolfram Sperber. Text analysis  in mathematics -
  the DeLiVerMATH project
- Sebastian Bönisch, Michael Brickenstein, Hagen Chrapary, Gert-Martin
  Greuel and Wolfram  Sperber. swMATH - a new  service for mathematics
  software
- Christoph Lüth  and Martin Ring.  A Web Interface for  Isabelle: The
  Next Generation
- Michal   Růžička,  Petr   Sojka  and   Vlastimil   Krejčíř.  Towards
  Machine-Actionable Modules of a Digital Mathematics Library

Registration is online via

http://cicm-conference.org/2013/cicm.php?event=&menu=registration

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Looking for old CAV pictures for the website and the brochure

*******Apologies if you receive this request more than once.***************

We are looking for old CAV pictures to use in CAV 2013 brochures and
presentations.

If you have pictures you took in CAV in the past, we would really
appreciate if you can send them to Katarina Jurik at jurik <at> forsyte.at.

Please state explicitly that you do not object to your pictures being used
on the website and in the printed media.

Many thanks, and see you at CAV 2013!

Hana Chockler
CAV 2013 Publicity Chair
On behalf of CAV 2013 Organizing Committee

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j

[Deadline extended: June 15] CFP: Workshop on Knowledge Representation and Reasoning in Robotics <at> ICLP2013, Istanbul, Turkey

(Apologies for cross-posting.)

CALL FOR PAPERS AND POSTER ABSTRACTS

Workshop on Knowledge Representation and Reasoning in Robotics
at the International Conference on Logic Programming (ICLP).

Location: Istanbul, Turkey.
Date of Workshop: August 25, 2013.

Workshop web site:

	http://www.cs.ttu.edu/~smohan/krr_iclp13/
	
Conference web site:

	http://www.iclp2013.org/en/default.asp

WORKSHOP SCOPE

Mobile robots (and agents) are increasingly being used in a range
of application domains such as disaster rescue, surveillance,
health care and navigation. A formidable challenge to the
widespread deployment of robots in our homes, offices and other
complex domains is the ability to represent, reason with and
revise incomplete and inconsistent domain knowledge obtained from
sensor inputs and high-level human feedback. Although many
algorithms have been developed for representing and reasoning
with domain knowledge, the research community is fragmented, with
separate vocabularies that are increasingly (and ironically)
making it difficult for these researchers to communicate with
each other. As a result, the rich body of research in knowledge
representation for cognitive agents is not fully exploited by
robotics researchers. For instance, declarative programming
paradigms provide non-monotonic reasoning capabilities essential
for robotics, although they do not always consider the challenge
of modeling the uncertainty in robot application domains. In
parallel, many robotics researchers are developing probabilistic
reasoning algorithms that elegantly model the uncertainty in
sensing and navigation on robots, although it is a challenge to
use such algorithms to represent and reason with commonsense
knowledge. In recent years, algorithms have also been developed
for combining logical and probabilistic reasoning, but these
algorithms do not support the desired knowledge representation
and reasoning capabilities, or fail to address problems (e.g.,
frame problem, ramification problem) that are well understood in
the logic programming community.

This workshop seeks to engage the logic programming community in
robotics research challenges. The objective is to promote a
deeper understanding of recent breakthroughs and tough challenges
in the logical programming and probabilistic robotics
communities, resulting in collaborative efforts towards
addressing the knowledge representation and reasoning challenges
in robotics. Topics of interest include (but are not limited to):

 *  Knowledge acquisition and representation.
 *  Reasoning with incomplete and inconsistent knowledge.
 *  Reasoning about actions and change.
 *  Planning and scheduling.
 *  Learning and symbol grounding.
 *  Cognitive architectures.
 *  Multiagent systems. 

We are especially interested in papers describing efforts to
integrate knowledge representation, logical reasoning and/or
probabilistic reasoning on robots and agents in different
application domains.

PAPER SUBMISSION

Paper submissions can be in one of the following categories:

* Regular paper: the length of regular papers (including figures
  and bibliography) should not exceed 12 pages.

* Poster/summary paper: the length of poster/summary papers
  (including all figures and bibliography) should not exceed 4
  pages.

Papers must be written in English using the same format used for
ICLP submissions: http://www.iclp2013.org/en/Submissions.html

Easychair paper submission web site:

	https://www.easychair.org/conferences/?conf=krr2013

IMPORTANT DATES

Submission deadline:   June 15, 2013
Notifications:         June 30, 2013
Camera-ready deadline: July 10, 2013
Workshop at ICLP:      August 25, 2013

ORGANIZERS

Mohan Sridharan
Department of Computer Science
Texas Tech University, USA
http://www.cs.ttu.edu/~smohan/

Fangkai Yang
Department of Computer Sciences
The University of Texas at Austin, USA
http://www.cs.utexas.edu/~fkyang

Volkan Patoglu
Mechatronics Program
Faculty of Engineering and Natural Sciences
Sabanci University, Istanbul, Turkey
http://myweb.sabanciuniv.edu/vpatoglu/

Peter Schueller
Computer Science Program
Faculty of Engineering and Natural Sciences
Sabanci University, Istanbul, Turkey
http://www.peterschueller.com/

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j

CICM 2013: Final Call for Work in Progress Papers, Deadline June 7th, 2013

     CICM 2013 - Conferences on Intelligent Computer Mathematics
         July 8-12, 2013 at University of Bath, Bath, UK

           http://www.cicm-conference.org/2013/cicm.php

		Final Call for Work-in-Progress Papers

----------------------------------------------------------------------
* Final call for Work-In-Progress Papers on any CICM topic
* Submissions 5-10 pages, for poster/talk presentations
* Deadline 7th June, notification 20th June

* Invited Talks by
  Patrick Ion (Mathematical Reviews, American Mathematical
               Society, USA)
  Assia Mahboubi (École Polytechnique and  INRIA/Microsoft
	                Research Joint Centre, France)
  Ursula Martin (Queen Mary, University of London, UK)
* Accepted regular papers are online on the website
* Co-Located Workshops:
  - MathUI'13: Mathematical User Interfaces
  - OpenMath Workshop 2013
  - PLMMS'13: Programming Languages for Mechanized Mathematics Systems
  - THedu'13: TP Components for Educational Software
----------------------------------------------------------------------

As   computers   and   communications  technology   advance,   greater
opportunities  arise for  intelligent mathematical  computation. While
computer  algebra, automated  deduction,  mathematical publishing  and
novel user interfaces individually have long and successful histories,
we  are now seeing  increasing opportunities  for synergy  among these
areas. The  Conferences on  Intelligent Computer Mathematics  offers a
venue for discussing these areas and their synergy.

The   conference  will   take  place   at  the   University   of  Bath
(www.bath.ac.uk),  with James  Davenport  as the  local organiser.  It
consists of four tracks:

Calculemus
  Chair: Wolfgang Windsteiger
Digital Mathematical Libraries (DML)
  Chair: Petr Sojka
Mathematical Knowledge Management (MKM)
  Chair: David Aspinall
Systems and Projects
  Chair: Christoph Lange

As  in  previous  years,  there  will  be  a  Doctoral  Programme  for
presentations by Doctoral students.

The  overall  programme is  organised  by  the  General Program  Chair
Jacques Carette.

----------------------------------------------------------------------
                          Important dates
----------------------------------------------------------------------

WiP paper submission deadline        :     7 June 2013
WiP paper Notification of acceptance :    20 June 2013
WiP Camera ready copies due          :     5 July 2013
Conference                           :  8-12 July 2013

----------------------------------------------------------------------
                               Tracks
----------------------------------------------------------------------

==========
Calculemus
==========

Calculemus   2013  invites   the  submission   of   original  research
contributions to be considered for publication and presentation at the
conference.  Calculemus  is a series  of conferences dedicated  to the
integration  of  computer  algebra   systems  (CAS)  and  systems  for
mechanised  reasoning  like   interactive  proof  assistants  (PA)  or
automated theorem  provers (ATP).  Currently,  symbolic computation is
divided into several (more  or less) independent branches: traditional
ones  (e.g., computer  algebra and  mechanised reasoning)  as  well as
newly emerging ones (on  user interfaces, knowledge management, theory
exploration, etc.) The main concern  of the Calculemus community is to
bring these  developments together in order to  facilitate the theory,
design,  and  implementation   of  integrated  mathematical  assistant
systems  that  will  be  used routinely  by  mathematicians,  computer
scientists and  all others who need  computer-supported mathematics in
their every day business.

All  topics  in  the  intersection  of computer  algebra  systems  and
automated  reasoning systems  are  of interest  for Calculemus.  These
include but are not limited to:

* Automated theorem proving in computer algebra systems.
* Computer algebra in theorem proving systems.
* Adding reasoning capabilities to computer algebra systems.
* Adding computational capabilities to theorem proving systems.
* Theory, design and implementation of interdisciplinary systems for
computer mathematics.
* Case studies and applications that involve a mix of computation and
reasoning.
* Case studies in formalization of mathematical theories.
* Representation of mathematics in computer algebra systems.
* Theory exploration techniques.
* Combining methods of symbolic computation and formal deduction.
* Input languages, programming languages, types and constraint languages,
and modeling languages for mathematical assistant systems.
* Homotopy type theory.
* Infrastructure for mathematical services.

===
DML
===

Mathematicians dream of a digital archive containing all peer-reviewed
mathematical literature ever published, properly linked, validated and
verified.   It is  estimated that  the entire  corpus  of mathematical
knowledge  published over  the centuries  does not  exceed 100,000,000
pages,   an   amount   easily   manageable  by   current   information
technologies.

Track objective  is to provide  a forum for development  of math-aware
technologies, standards, algorithms and formats towards fulfillment of
the  dream  of global  digital  mathematical  library (DML).  Computer
scientists  (D)  and librarians  of  digital  age  (L) are  especially
welcome to  join mathematicians  (M) and discuss  many aspects  of DML
preparation.

Track topics  are all topics of mathematical  knowledge management and
digital  libraries  applicable  in  the  context of  DML  building  --
processing of math knowledge expressed in scientific papers in natural
languages, namely:

* Math-aware text mining (math mining) and MSC classification
* Math-aware representations of mathematical knowledge
* Math-aware computational linguistics and corpora
* Math-aware tools for [meta]data and fulltext processing
* Math-aware OCR and document analysis
* Math-aware information retrieval
* Math-aware indexing and search
* Authoring languages and tools
* MathML, OpenMath, TeX and other mathematical content standards
* Web interfaces for DML content
* Mathematics on the web, math crawling and indexing
* Math-aware document processing workflows 
* Archives of written mathematics
* DML management, business models
* DML rights handling, funding, sustainability 
* DML content acquisition, validation and curation 

===
MKM
===

Mathematical  Knowledge Management  is an  interdisciplinary  field of
research in the intersection of mathematics, computer science, library
science, and scientific publishing. The objective of MKM is to develop
new and better ways  of managing sophisticated mathematical knowledge,
based on innovative technology  of computer science, the Internet, and
intelligent   knowledge   processing.  MKM   is   expected  to   serve
mathematicians,  scientists,   and  engineers  who   produce  and  use
mathematical  knowledge; educators  and students  who teach  and learn
mathematics;   publishers  who   offer   mathematical  textbooks   and
disseminate   new    mathematical   results;   and    librarians   and
mathematicians who catalog and organize mathematical knowledge.

The conference is concerned with all aspects of mathematical knowledge
management. A non-exclusive list of important topics includes:

 * Representations of mathematical knowledge
 * Authoring languages and tools
 * Repositories of formalized mathematics
 * Deduction systems
 * Mathematical digital libraries
 * Diagrammatic representations
 * Mathematical OCR
 * Mathematical search and retrieval
 * Math assistants, tutoring and assessment systems
 * MathML, OpenMath, and other mathematical content standards
 * Web presentation of mathematics
 * Data mining, discovery, theory exploration
 * Computer algebra systems
 * Collaboration tools for mathematics
 * Challenges and solutions for mathematical workflows

====================
Systems and Projects
====================

The  Systems and  Projects  track of  the  Conferences on  Intelligent
Computer Mathematics  is a forum for presenting  available systems and
new and ongoing  projects in all areas and topics  related to the CICM
conferences:

* Deduction and Computer Algebra (Calculemus)
* Digital Mathematical Libraries (DML)
* Mathematical Knowledge Management (MKM)
* Artificial Intelligence and Symbolic Computation (AISC)

The track aims  to provide an overview of  the latest developments and
trends within the CICM community  as well as to exchange ideas between
developers and introduce systems to an audience of potential users.

----------------------------------------------------------------------
                       Submission Instructions
----------------------------------------------------------------------

Work-in-progress submissions  are intended to provide a  forum for the
presentation of original work that is not (yet) in a suitable form for
submission as a  full or system description paper.  This includes work
in progress  and emerging  trends. Their size  is not limited,  but we
recommend 5-10 pages.

Accepted work-in-progress  papers will be presented  at the conference
as  short   teaser  talks   and  as  posters.    The  work-in-progress
proceedings will be published online with CEUR-WS.org.

WiP papers should be prepared in LaTeX and formatted according to the
requirements of Springer's LNCS series (the corresponding style files
can be downloaded from
http://www.springer.de/comp/lncs/authors.html). By  submitting a paper
the authors agree  that if it is accepted at least  one of the authors
will attend the conference to present it.

Electronic submission is done through easychair 
http://www.easychair.org/conferences/?conf=cicm2013

----------------------------------------------------------------------
                       Programme Committee
----------------------------------------------------------------------

Akiko Aizawa, NII, The University of Tokyo, Japan
Jesse Alama, CENTRIA, FCT, Universidade Nova de Lisboa, Portugal
Rob Arthan, Queen Mary University of London, UK
Andrea Asperti, University of Bologna, Italy
David Aspinall, University of Edinburgh, UK
Jeremy Avigad, Carnegie Mellon University, US
Thierry Bouche, Université Joseph Fourier (Grenoble), France
Jacques Carette, McMaster University, Canada
John Charnley, Department of Computing, Imperial College London, UK
Janka Chlebíková, School of Computing, University of Portsmouth, UK
Simon Colton, Department of Computing, Imperial College, London, UK
Leo Freitas, Newcastle University, UK
Deyan Ginev, Jacobs University Bremen, Germany
Gudmund Grov, Heriot-Watt University, Edinburgh, UK
Thomas Hales, University of Pittsburgh, US
Yannis Haralambous, Télécom Bretagne, France 
Jónathan Heras, University of Dundee, UK
Hoon Hong, North Carolina State University, US
Predrag Janičić, University of Belgrade, Serbia
Cezary Kaliszyk, University of Innsbruck, Austria
Manfred Kerber, University of Birmingham, UK
Adam Kilgarriff, Lexical Computing Ltd, UK
Andrea Kohlhase, Jacobs University Bremen, Germany
Michael Kohlhase, Jacobs University Bremen, Germany
Temur Kutsia, RISC Institute, JKU Linz, Austria
Christoph Lange, University of Birmingham, UK
Paul Libbrecht, Martin Luther University Halle-Wittenberg, Germany
Christoph Lüth, DFKI Bremen, Germany
Till Mossakowski, DFKI Bremen, Germany
Magnus O. Myreen, University of Cambridge, UK
Florian Rabe, Jacobs University Bremen, Germany
Jiří Rákosník, Institute of Mathematics, Academy of Sciences, Czech Republic
Carsten Schuermann, IT University of Copenhagen, Denmark
Petr Sojka, Masaryk University, Faculty of Informatics, Czech Republic
Hendrik Tews, TU Dresden, Germany
Frank Tompa, University of Waterloo, Canada
Josef Urban, Radboud University, Netherlands
Stephen Watt, University of Western Ontario, Canada
Makarius Wenzel, Université Paris-Sud 11, France
Wolfgang Windsteiger, RISC Institute, JKU Linz, Austria
Richard Zanibbi, Rochester Institute of Technology, US

--

Dr. Serge Autexier, serge.autexier <at> dfki.de, http://www.dfki.de/~serge/
Research Department Cyber-Physical Systems
MZH, Room 3120                             Phone: +49 421 218    59834
Bibliothekstr.1, D-28359 Bremen              Fax: +49 421 218 98 59834
----------------------------------------------------------------------
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313 
----------------------------------------------------------------------

------------------------------------------------------------------------------
How ServiceNow helps IT people transform IT departments:
1. A cloud service to automate IT design, transition and operations
2. Dashboards that offer high-level views of enterprise services
3. A single system of record for all IT processes
http://p.sf.net/sfu/servicenow-d2d-j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info