Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root

For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is deductive proof. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in the automotive embedded software.

Die Dichotomie analytisch-synthetisch bei Frege unter Berücksichtigung von Kant

I begin by commenting on Kant’s conception of analytic judgements. I then turn to Frege’s notion of analyticity. I argue that his definition of analytic truth in terms of provability from logical axioms and definitions is incomplete. The requisite analyticity of the logical axioms and the definitions, and accordingly the required justification of acknowledging them as true, must be explained in a non-deductive way. I further argue that analyticity in terms of deductive proof deviates significantly from Kant’s conception of analytic judgements. I conclude with two case studies. The first concerns Frege’s attempted justification of the synthetic nature of the geometrical axioms. The second deals with Hume’s Principle, which in his logicist project Frege must establish as an analytic truth.

Rewriting and Well-Definedness within a Proof System

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.

Black Thoughts Matter

In postapartheid South Africa, Whites dominate academics and Black students are agitating for decolonization. Decolonization requires contesting the false history of science used to set up colonial education essential to colonization—the same false history that was used to morally justify racism, by asserting the noncreativity of Blacks. The “evidence” for this false history is often faith-based, so White-controlled academics disallows any open discussion. Furthermore, this false history is sustained by another trick: a little known interplay between history and philosophy. Thus, geometry has been credited to Greeks on the ground that they had a “superior” philosophy of mathematics as deductive proof. In fact, the “Pythagorean” proposition had no valid deductive proof before the 20th century. Furthermore, this claim of philosophical “superiority” was never academically debated, and is not allowed to be. A recent attempt to explain the falsehood of this claim, along with the counterevidence against purported Greek achievements in math, was publicly censored. In fact, in Egypt, Iraq, and India, there was a different and immensely superior understanding of the “Pythagorean” proposition, which superior way was not grasped in the West, resulting in its persistent navigational problems until the late 18th century.