[Hol-info] Isabelle/HOL and Division by zero

[Saburou Saitoh]

Isabelle/HOL and Division by zero:



Dear the related persons:



Professor Larry Paulson kindly stated in his e-mail to me that: The idea
that x/0 = 0 is only a convention. It does not change mathematics in any
significant way and it does not lead to contradictions either. On 2017/07/04
 0:2

Jose kindly introduced the relation of Isabelle/HOL and Division by zero,
in details:



Thank you for the book. Attached to this email you will find the discussion
between Prof. Lawrence Paulson (*https://www.cl.cam.ac.uk/~lp15/*
<#m_-7616739960837325088_search/isabelle/_blank>) and Prof. Harvey
Friedman (*https://math.osu.edu/people/friedman.8*
<#m_-7616739960837325088_search/isabelle/_blank>) concerning the division
by zero.



I understand Isabelle/HOL derived the result 1/0=0 about 40 years ago,
however, nobody did not understand its importance over the system, for this
essence, please look the survey draft:



 *viXra:1908.0100*  submitted on 2019-08-06
20:03:01, (922 unique-IP downloads)

Fundamental of Mathematics; Division by Zero Calculus and a New Axiom

I have the general questions:



1) The definition and motievation of 1/0=0 by Isabelle.

2) Why is it conventional?



I think for the division by zero, the definition is very essential and
important, because in the usual definition we have a contradiction,
immediately.



I feel that Isabelle/HOL creates many new worlds.



With best regards,

Sincerely yours,

Saburou Saitoh

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

[Hol-info] [CfP] SAT2020 - The 23rd International Conference on , , Theory and Applications of Satisfiability Testing

[Luca Pulina]

 Call for Papers 


   The 23rd International Conference on

 Theory and Applications of Satisfiability Testing

   (SAT 2020)


 5-9 July 2020, Alghero, Italy


 http://sat2020.idea-researchlab.org/


*


The International Conference on Theory and Applications

of Satisfiability Testing (SAT) is the premier annual

meeting for researchers focusing on the theory and

applications of the propositional satisfiability problem,

broadly construed. In addition to plain propositional

satisfiability, it also includes Boolean optimization

(such as MaxSAT and Pseudo-Boolean (PB) constraints),

Quantified Boolean Formulas (QBF), Satisfiability Modulo

Theories (SMT), and Constraint Programming (CP) for

problems with clear connections to Boolean-level reasoning.



*** Scope ***


SAT 2020 welcomes scientific contributions addressing

different aspects of the satisfiability problem, interpreted

in a broad sense. Topics include, but are not restricted to:


* Theoretical advances

* Practical search algorithms

* Knowledge compilation

* Implementation-level details of SAT solving tools

* Problem encodings and reformulations

* Applications

* Case studies based on rigorous experimentation



*** Out of Scope ***


Papers claiming to resolve a major long-standing open

theoretical question in Mathematics or Computer Science

(such as those for which a Millennium Prize is offered),

are outside the scope of the conference because there is

insufficient time in the schedule to referee such papers;

instead, such papers should be submitted to an appropriate

technical journal.



*** Paper Categories ***


Submissions to SAT 2020 are solicited in three categories,

describing original contributions.


* Long papers (9 to 15 pages, excluding references)

* Short papers (up to 8 pages, excluding references)

* Tool papers (up to 6 pages, excluding references)


Long and short papers should contain original research, with

sufficient detail to assess the merits and relevance of the

contribution. For papers reporting experimental results, authors

are strongly encouraged to make their data and implementations

available with their submission.


Submissions on applications and cases studies are especially

welcome. Such papers should describe details, weaknesses

and strengths of the considered approaches in sufficient depth,

but they are not expected to introduce novel solving approaches.


Tool papers must obey to specific content criteria. A tool

paper should describe the implemented tool and its novel

features. Here “tools” are interpreted in a broad sense,

including descriptions of implemented solvers, preprocessors,

etc. as well as systems that exploit SAT solvers or their

extensions for use in interesting problem domains.


A demonstration is expected to accompany a tool presentation.

Papers describing tools that have already been presented

previously are expected to contain significant and clear

enhancements to the tool.


Long and short papers will be evaluated with the same quality

standards, and are expected to contain a similar contribution

per page ratio.




*** Submissions ***


Submissions should not be under review elsewhere nor be submitted 
elsewhere while under review for SAT 2020, and should not consist of 
previously published material.



Submissions not consistent with the above guidelines may be returned 
without review.



All papers submissions are done exclusively via EasyChair in Springer’s 
LaTeX llncs2e style.



One author of each accepted paper is expected to present it at the 
conference.



Further details can be found at the website of SAT 2020:

http://sat2020.idea-researchlab.org/



*** Proceedings ***


The proceedings will be published by Springer in the series Lecture 
Notes in Computer Science, seewww.springer.com/lncs 
.




*** Important Dates ***


Workshops                July 5, 2020

Conference               July 6-9, 2020


Abstract submission      February 15, 2020

Paper submission         February 22, 2020

Author response period   March 29 – April 2, 2020

Author notification      April 18, 2020

Camera-ready             May 3, 2020



*** Organization ***



Program Chairs


* Luca Pulina, University of Sassari

* Martina Seidl, Johannes Kepler University Linz



Workshop Chair


* Florian Lonsing, Stanford University



Publicity Chair


* Laura Pandolfo, University of Sassari



Program Committee


* Fahiem Bacchus, University of Toronto

* Olaf Beyersdorff, Friedrich Schiller University Jena

* Armin Biere, Johannes Kepler University Linz

* Nikolaj Bjorner, Microsoft

* Maria Luisa Bonet, Universitat Politècnica de Catalunya

* Sam Buss, University of California San Diego

* Florent Capelli, Université de Lille

* Pascal Fontaine, Université de Liège, Belgium

* Marijn