Related papers: A correspondence problem for mathematical proof
The theory of actual causality, defined by Halpern and Pearl, and its quantitative measure - the degree of responsibility - was shown to be extremely useful in various areas of computer science due to a good match between the results it…
Formal explainability guarantees the rigor of computed explanations, and so it is paramount in domains where rigor is critical, including those deemed high-risk. Unfortunately, since its inception formal explainability has been hampered by…
In this paper we propose a new perspective on the evolution and history of the idea of mathematical proof. Proofs will be studied at three levels: syntactical, semantical and pragmatical. Computer-assisted proofs will be give a special…
In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of…
The features of a logically sound approach to a theory of statistical reasoning are discussed. A particular approach that satisfies these criteria is reviewed. This is seen to involve selection of a model, model checking, elicitation of a…
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify a given one). (2) Under the assumption that Knuth-Bendix…
We survey some results that provide different versions of classical results through different summability methods. Specifically, in order to adapt such classical results, we analyze which properties should satisfy the summability methods.…
There are various approaches to the problem of how one is supposed to conduct a statistical analysis. Different analyses can lead to contradictory conclusions in some problems so this is not a satisfactory state of affairs. It seems that…
In Mathematics is common to make a mistake and therefore a false conclusion arises. In each case it is important to recognize the mistake in order to avoid a similar one in the future. Geometric figures provide decisive help in order to…
Verifying mathematical proofs is difficult, but can be automated with the assistance of a computer. Autoformalization is the task of automatically translating natural language mathematics into a formal language that can be verified by a…
The idea of fully accepting statements when the evidence has rendered them probable enough faces a number of difficulties. We leave the interpretation of probability largely open, but attempt to suggest a contextual approach to full belief.…
Model theoretic results such as Characterization and Definability give important information about different logics. It is well known that the proofs of those results for several modal logics have, somehow, the same 'taste'. A general proof…
This article examines two approaches to verification, one based on using a logic for expressing properties of a system, and one based on showing the system equivalent to a simpler system that obviously has whatever property is of interest.…
Language models are increasingly being used in important decision pipelines, so ensuring the correctness of their outputs is crucial. Recent work has proposed evaluating the "factuality" of claims decomposed from a language model generation…
Modern mathematics is known for its rigorous proofs and tight analysis. Math is the paradigm of objectivity for most. We identify the source of that objectivity as our knowledge of the physical world given through our senses. We show in…
We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math dictations", presents users with the task of formalizing a…
Constructivists (and intuitionists in general) asked what kind of mental construction is needed to convince ourselves (and others) that some mathematical statement is true. This question has a much more practical (and even cynical)…
Traditional treatments of formal logic provide: 1. A syntax for formulas. 2. An inference relation between sets of formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. First…
Axiomatizing mathematical structures is a goal of Mathematical Logic. Axiomatizability of the theories of some structures have turned out to be quite difficult and challenging, and some remain open. However axiomatization of some…
In this note some philosophical thoughts and observations about mathematics are expressed, arranged as challenges to some common claims.