相关论文: Number Theory and Axiomatic Geometry in the Diproc…

In this article we address the problem of automatic answer checking in interactive learning systems that support mathematical notation. This problem consists of the problem of establishing identities in formal mathematical systems and hence…

If we want mathematics education to be valuable to everybody, including those who do not pursue mathematics-related careers, we need to use mathematics as a training ground for certain ways of thinking. This dissertation focuses on one…

LangPro is an automated theorem prover for natural language (https://github.com/kovvalsky/LangPro). Given a set of premises and a hypothesis, it is able to prove semantic relations between them. The prover is based on a version of analytic…

We report on several scenarios of using automated theorem proving software in university education. In particular, we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial…

We present IntelliProof, an interactive system for analyzing argumentative essays through LLMs. IntelliProof structures an essay as an argumentation graph, where claims are represented as nodes, supporting evidence is attached as node…

The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual…

This paper tries to justify the relevance of an introductory course in Mathematical Logic in the Philosophy curriculum for analyzing philosophical arguments in natural language. It is argued that the representation of the structure of…

Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. The main issues are the correct use of formal language and…

We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their…

Deductive coding is a common discourse analysis method widely used by learning science and learning analytics researchers for understanding teaching and learning interactions. It often requires researchers to manually label all discourses…

A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to…

The combination of verifiable languages and LLMs has significantly influenced both the mathematical and computer science communities because it provides a rigorous foundation for theorem proving. Recent advancements in the field provide…

In this work, I present an automatic system for the evaluation of closed-type exercises in physics at the high school level or in the first year of a degree where physics is a mandatory course. It is expected that this will allow students…

We exhibit differential geometric structures that arise in numerical methods, based on the construction of Cauchy sequences, that are currently used to prove explicitly the existence of weak solutions to functional equations. We describe…

A comparison of the "theory of random sequences" developed during the twentieth century and the axiomatic approach of probability theory proposed by Kolmogorov shows the importance of sigma-additivity as extension tool. Similarly, the…

Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata…

Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an…

This is an attempt to present axioms for Euclidean geometry, aiming at the following goals: to work with geometric notions (thus not merely identify points with pairs of numbers, giving a special status to a particular coordinate system);…

There is a sharp disconnect between the programming and mathematical portions of the standard undergraduate computer science curriculum, leading to student misunderstanding about how the two are related. We propose connecting the subjects…

Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves…