scholarly journals Challenge to the proving of theorems of Euclid's elements of as ATP

2019 ◽  
Vol 3 (4) ◽  
pp. 9-13
Author(s):  
Keyword(s):  
Mathematical Logic ◽  
Mathematics Education ◽  
Theorem Proving ◽  
Automated Reasoning ◽  
Automated Theorem Proving ◽  
Euclidean Geometry ◽  
Proof Assistant ◽  
Weak Point ◽  
Euclid’S Elements ◽  
Generic Proof

Automated theorem proving (ATP) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. An Isabelle/HOL is a generic proof assistant. We perform the challenge for the proving theorems of Euclid's elements of geometry. We could prove some theorems of Euclid's elements of geometry. Technique of programing and mental conception interact. The mathematics education which prove theorems of the Euclidean geometry by using the Isabelle/HOL can correct the present weak point

Proving in Mathematics Education – On the Proof using ATP

2019 ◽  
pp. 558-563
Author(s):  
Tadashi Takahashi
Keyword(s):  
Mathematics Education ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Mathematical Thinking ◽  
Present Situation ◽  
Point Of View ◽  
Clear Vision ◽  
Euclid’S Elements ◽  
A Chain

The aim of the mathematics education is the acquisition of “knowledge/skill of the mathematics” and “the mathematical thinking”. Proving is a chain of the logic in mathematics and is “mathematical thinking” itself. So, proving is the domain that is important from a point of view that can evaluate the acquisition of enough “mathematical thinking”. There is a variety of sense of values in the present situation of the proof using the ATP (Automated theorem proving). We should establish a clear vision as mathematics education in this situation. That is, in mathematics education, we should build sense of values for proof using the ATP newly. To that end, we fix contents of the mathematics, and it is necessary to prove them by using ATP. We would like to assume the aim the theorems of Euclid's Elements. Because the contents are the basics of the mathematical thinking. The proving is an important aim in the mathematics education, it is necessary to clarify new value by using the ATP as mathematics education.

scholarly journals Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL

10.29007/4dsr ◽  
2018 ◽  
Author(s):  
Alexander Steen ◽  
Max Wisniewski ◽  
Christoph Benzmüller
Keyword(s):  
Artificial Intelligence ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Description Logics ◽  
Automated Analysis ◽  
Higher Order ◽  
Order Logic ◽  
Proof Assistant ◽  
Higher Order Logic ◽  
Multimodal Logics

Non-classical logics (such as modal logics, description logics, conditional logics, multi-valued logics, hybrid logics, etc.) have many applications in artificial intelligence. In this tutorial, we will demonstrate a generic approach to automate propositional and quantified variants of non-classical logics using theorem proving systems for classical higher-order logic. Our particular focus will be on quantified multimodal logics. We will present and discuss a semantical embedding of quantified multimodal logics into classical higher-order logic, which enables the encoding and automated analysis of non-trivial modal logic problems in the Isabelle/HOL proof assistant. Additionally, TPTP compliant automated theorem proving systems can be called from within Isabelle’s Sledgehammer tool for automating reasoning tasks. In the tutorial, we will apply this approach to exemplarily solve a prominent puzzle from the AI literature: the well-known wise men.

scholarly journals Checking the quality of clinical guidelines using automated reasoning tools

2008 ◽  
Vol 8 (5-6) ◽  
pp. 611-641 ◽  
Author(s):  
ARJEN HOMMERSOM ◽  
PETER J. F. LUCAS ◽  
PATRICK VAN BOMMEL
Keyword(s):  
Theorem Proving ◽  
Clinical Guidelines ◽  
Automated Reasoning ◽  
Automated Theorem Proving ◽  
Interactive Theorem Proving ◽  
Theorem Prover ◽  
First Order ◽  
Medical Quality ◽  
Diabetes Mellitus 2

AbstractRequirements about the quality of clinical guidelines can be represented by schemata borrowed from the theory of abductive diagnosis, using temporal logic to model the time-oriented aspects expressed in a guideline. Previously, we have shown that these requirements can be verified using interactive theorem proving techniques. In this paper, we investigate how this approach can be mapped to the facilities of a resolution-based theorem prover,otterand a complementary program that searches for finite models of first-order statements,mace-2. It is shown that the reasoning required for checking the quality of a guideline can be mapped to such a fully automated theorem-proving facilities. The medical quality of an actual guideline concerning diabetes mellitus 2 is investigated in this way.

The 10th IJCAR automated theorem proving system competition – CASC-J10

2021 ◽  
pp. 1-15
Author(s):  
Geoff Sutcliffe
Keyword(s):  
Theorem Proving ◽  
Classical Logic ◽  
Automated Theorem Proving ◽  
Fully Automatic

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J10 was the twenty-fifth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition divisions. This paper presents an outline of the competition design, and a commentated summary of the results.

Retrieval System and Dynamic Algorithm Looking for Axioms of Notions Defined by Programs

1993 ◽  
Vol 19 (3-4) ◽  
pp. 275-301
Author(s):  
Andrzej Biela
Keyword(s):  
Theorem Proving ◽  
Dynamic Process ◽  
Functional Equations ◽  
Automated Theorem Proving ◽  
Retrieval System ◽  
Formal System ◽  
Dynamic Algorithm ◽  
Algorithmic Logic ◽  
Correctness Of Programs

In this paper we shall introduce a formal system of algorithmic logic which enables us to formulate some problems connected with a retrieval system which provides a comprehensive tool in automated theorem proving of theorems consisting of programs, procedures and functions. The procedures and functions may occur in considered theorems while the program of the above mentioned system is being executed. We can get an answer whether some relations defined by programs hold and we can prove functional equations in a dynamic way by looking for a special set of axioms /assumptions/ during the execution of system. We formulate RS-algorithm which enables us to construct the set of axioms for proving some properties of functions and relations defined by programs. By RS-algorithm we get the dynamic process of proving functional equations and we can answer the question whether some relations defined by programs hold. It enables us to solve some problems concerning the correctness of programs. This system can be used for giving an expert appraisement. We shall provide the major structures and a sketch of an implementation of the above formal system.

scholarly journals Preface

2011 ◽  
Vol 21 (4) ◽  
pp. 671-677 ◽  
Author(s):  
GÉRARD HUET
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
20Th Century ◽  
Theorem Proving ◽  
Propositional Calculus ◽  
Interactive Theorem Proving ◽  
Predicate Calculus ◽  
Special Issue ◽  
Mathematical Structures ◽  
Infinite Domains

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.

scholarly journals Um Passeio pelo Labirinto da Lógica Matemática em companhia de Malba Tahan

2018 ◽  
Vol 15 (19) ◽  
pp. 247-264
Author(s):  
Inocêncio Fernandes Balieiro Filho
Keyword(s):  
Mathematical Logic ◽  
Euclidean Geometry ◽  
History Of Mathematics ◽  
Logical Structure ◽  
Deductive System ◽  
Axiomatic Method ◽  
Concept Definition ◽  
History Of ◽  
Contemporary Approach

O presente artigo tem por objetivo discutir numa perspectiva contemporânea os conteúdos de Lógica, Matemática, Filosofia da Matemática e História da Matemática presentes no livro A Lógica na Matemática, escrito por Malba Tahan. Para isso, mediante o uso da historiografia, foram selecionados temas concernentes com os assuntos da pesquisa. Foram tratados os seguintes temas: a base lógica da Matemática, a definição de conceito, os princípios para se definir um objeto, as definições e a natureza dos axiomas em Matemática, o método axiomático e as diversas axiomáticas para a geometria euclidiana, a estrutura lógica de um sistema dedutivo, os métodos de demonstração em Matemática, a indução, analogia e dedução em Matemática.   Palavras-chave: Lógica Matemática; História da Matemática; Filosofia da Matemática.   A TOUR BY THE LABYRINTH OF MATHEMATICAL LOGIC IN THE COMPANY OF MALBA TAHAN   Abstract   In this paper we discuss the Mathematics, the Logic of Mathematics, the Philosophy and History of Mathematics that presents in the book A Lógica na Matemática of the Malba Tahan, in a contemporary approach. For that, we use the historiography to select matters in adherence with the research. Are treated this topics: the basis of the Logic of Mathematics; the concept definition; principles to define an object; definitions and nature of the axioms in Mathematics; the axiomatic method and the diverse axiomatic to the Euclidean Geometry; the logical structure of a deductive system; demonstration methods in mathematics; the induction, analogy and deduction in mathematics.  

Sign in / Sign up

Export Citation Format

Share Document