Search
Search Results
-
Relaxed Weighted Path Order in Theorem Proving
We propose an extension of the automated theorem prover E by the weighted path ordering (WPO). WPO is theoretically stronger than all the orderings...
-
Human and automated approaches for finite trigonometric sums
We show that identities involving trigonometric sums recently proved by Harshitha, Vasuki and Yathirajsharma, using Ramanujan’s theory of theta...
-
Is Computer Algebra Ready for Conjecturing and Proving Geometric Inequalities in the Classroom?
We introduce an experimental version of GeoGebra that successfully conjectures and proves a large scale of geometric inequalities by providing an...
-
Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch’s trick
In the algebraic-geometry-based theory of automated proving and discovery, it is often required that the user includes, as complementary hypotheses,...
-
Automated Theorem Proving Practice with Null Geometric Algebra
This paper presents the practice of automated theorem proving in Euclidean geometry with null geometric algebra, a combination of Conformal Geometric...
-
Using Isabelle in Two Courses on Logic and Automated Reasoning
We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The...
-
Substitutive Systems and a Finitary Version of Cobham’s Theorem
We study substitutive systems generated by nonprimitive substitutions and show that transitive subsystems of substitutive systems are substitutive....
-
From the String Landscape to the Mathematical Landscape: A Machine-Learning Outlook
We review the recent programme of using machine-learning to explore the landscape of mathematical problems. With this paradigm as a model for human...
-
Automatic conjecturing and proving of exact values of some infinite families of infinite continued fractions
Inspired by the recent pioneering work, dubbed “The Ramanujan Machine” by Raayoni et al. (The Ramanujan Machine: Automatically Generated Conjectures...
-
Andrews Skolemization May Shorten Resolution Proofs Non-elementarily
In this paper we construct a sequence of formulas \(F_1, F_2, \ldots \)...
-
Logical Foundations of Computer Science International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13, 2022, Proceedings
This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2022, held in...
-
Self-evident Automated Proving Based on Point Geometry from the Perspective of Wu’s Method Identity
The algebraic methods represented by Wu’s method have made significant breakthroughs in the field of geometric theorem proving. Algebraic proofs...
-
Automated Analytic Combinatorics
We nowturn to the task of automating the asymptotic methods discussed in Chapter 5. A generic rational function has a smooth singular set and admits...
-
Proofs as Objects
The rigor of mathematics lies in its systematic organization that supports conclusive proofs of assertions on the basis of assumed principles. Proofs...
-
Note on a simple trigonometric equality
In a recent paper Vinay, Shweta, and Harshitha use Ramanujan’s theta functions to prove several trigonometric equalities. Elementary proofs for some...
-
Zilber’s Theorem for planar lattices, revisited
Zilber’s Theorem states that a finite lattice L is planar if and only if it has a complementary order relation. We provide a new proof for this...
-
Automated Deduction and Knowledge Management in Geometry
Scientific research and education at all levels are concerned primarily with the discovery, verification, communication, and application of...
-
Ramsey Theory Before Ramsey: Schur’s Coloring Solution of a Colored Problem and Its Generalizations
Nobody remembered – if anyone even noticed – Hilbert’s 1892 lemma by the time the second Ramseyan type result appears in 1916 in number theory as...
-
Thinking Programs Logical Modeling and Reasoning About Languages, Data, Computations, and Executions
This book describes some basic principles that allow developers of computer programs (computer scientists, software engineers, programmers) to...