text:
Vivica Zweidar
email: vivica@math.uni-bremen.de

Functions: Implicit

Keywords: Functions, classroom conversation, discourse analysis, implicit meaning, implicature

 concept of implicatures in order to analyse videotaped classroom conversation in a unit on functions. In this paper, I sketch the concept of implicitness in mathematics lessons.

Introduction

In my research on the implicit in classroom conversation about functions I seek to describe the discourse of learners and teachers in order to reveal the hidden, the unsaid, the implied meaning that has to be decoded to create and follow lessons sensibly. I want to characterize the interplay between the implicit in the mathematical object and the implicit in language when talking about functions. My research questions are: How are functions brought up in classroom conversation? And: What is the role of the implicit in classroom conversation in a unit on functions?

It is common sense that language is important for all school subjects. Mathematics is no exception (see for example [START_REF] Meyer | Sprachenvielfalt im Mathematikunterricht: Herausforderungen, Chancen, Förderansätze[END_REF] it is needed to get access to mathematical matters and to express mathematical concepts. Participating in classroom conversation and getting access to the mathematical content of mathematics lessons can become difficult for the participants on different levels. Apart from obstacles that are immanent in mathematical concepts there may be vocabulary or grammar difficulties, difficulties in the semantics as well as difficulties in a pragmatic sense when learning new contents. In my work, I focus on a pragmalinguistic perspective on classroom conversation about functions. This perspective takes into consideration that not only words or sentences are meaningful when talking but also the context of an utterance. Looking at language that way promises to reveal an unsaid meaning that can be found between the lines. The idea of making the unsaid or the unsayable come to the surface by analyzing the classroom discourse seems conveniently suitable to approach the processes in mathematics classrooms when abstract objects like functions are tried to be made accessible.

Didactical analysis

In order to link my language analysis to the mathematical content, I analyze the lessons and especially the classroom conversation on a didactical level at first. I seek to figure out what is presumably intended to be taught and learned about functions when working on different tasks and when talking about them.

Thematic Working Group 09

Proceedings of CERME10

The mathematical object function is very abstract. Looking at the historical development, the understanding of what a function is demonstrates how much functions are attached to their representations [START_REF] Malle | Aus der geschichte lernen[END_REF]. Till today in German classrooms functions are a central topic in the curriculum where traditionally the representations like algebraic expressions, graphs, tables of data and (realistic) situations of functional dependencies play an important role. [START_REF] Swan | The teaching of functions and graphs[END_REF] developed a model to describe the different activities, the so-called translation skills that have to be performed when transforming one representation into another. In my work, I categorize the classroom activities into sequences according to those translation skills. I focus especially on the skills that afford translating a representation of a function from or into situations that are generally closely linked to verbal descriptions. The activities when a representation is transformed from a situation can be summarized as modeling skills and activities when a representation is transformed into a situation can be summarized as interpretation skills.

Furthermore, different aspects of a function can become central in different tasks: you can classify the thinking about function into the following categories [START_REF] Vollrath | Funktionales Denken[END_REF]: functional dependency as a point wise relation, functional dependency as a dynamic process and functions viewed as objects or as a whole. The point wise relation takes into consideration that one independent element of a set gets mapped to one dependent element of a set, the dynamic process stands for the change that is produced in the dependent values when changing the independent values and functions as objects look at the given or produced correlation as a whole. Each activity or rather each translation skill can be performed on all of these three levels and form the second dimension for the didactical analysis of the lessons in my investigation.

In The example, I demonstrate how I work with this analysis in combination with the linguistic analysis in order to get a description of the implicit in the classroom conversation on functions.

Linguistic analysis

For the linguistic analysis, I use Grice's theory of conversation [START_REF] Grice | Logic and conversation[END_REF] as the background theory. Central in his theory are so-called implicaturesvery generally speaking an implicature is existent when something that is literally said by an utterance differs from what is meant by that utterance. An implicature analysis, as for example suggested by [START_REF] Hagemann | Implikaturanalyse[END_REF], reveals the implicit and what is likely to be meant and understood by the participants. [START_REF] Pimm | Mathematics classroom language: Form, function and force[END_REF] claims that Grice's implicatures are also relevant in classroom discourse and [START_REF] Rowland | Pragmatic perspectives on mathematics discourse[END_REF] presents analysis of students' utterances in mathematics discourse using Grice's ideas as a starting point for his theoretical framework.

Grice's concept of implicatures is based on the cooperation principle: Make your conversational contribution such as is required, at the stage at which it occurs, by the accepted purpose or direction of the talk exchange in which you are engaged (Grice, 1975, p. 45).

Under this assumption nothing that is uttered by a participant of a conversation is assumed to be meaningless and the speaker of the utterance supposes that the conversation partners can decode the utterance meaning. The cooperative principle is formulated very general and leads to more specific aspects about how understanding is produced in conversation. These aspects are the so-called conversational maxims. Grice formulates twelve maxims1 that are categorized into the maxims of quantity, quality, relation and manner. Whenever one of the maxims is violated this is a hint at the actual meaning of an utterance. While talking the flouting of maxims is an intuitive process that leads to understand an utterance in a specific way. An implicature analysis explains how a particular intuition is evoked. The following example illustrates the formation of an implicature by infringing the maxim of relation be relevant: The setting of the following conversation between two students is a lesson at school. The students are supposed to write down a solution to a textbook task.

(1) A:

I do not have a pencil. B:

My pencil case is on the table over there. In example (1) A implicates that she or he needs a pencil and B implicates that A can find one in the pencil case on the table. Both utterances only indirectly hint at the presumably intended meaning. The literal meaning is simply that one student does not have a pencil and that there is a pencil case on the table. The literal meaning is not very likely to be the intended meaning as this meaning would not be relevant in the given context. To confirm the presence of a conversational implicature in Grice's sense implicatures need to have two characteristicsnon-detachability and cancelability. These attributes can be tested as follows [START_REF] Korta | Implicatures: Cancelability and non-detachability[END_REF]: the implicature is non-detachable if you find synonym ways of saying the utterance without changing the implicature. In example (1) you could change A's utterance into "I do not hold a pencil." The implicature then remains that A needs a pencil. And the implicature is cancelable if you can neglect the implicature without producing a conflict with the literal meaning. For A in example (1) it is possible to say: "I do not have a pencil, but I do not mean that I need one. In fact, I do not want to write something down." Both utterances in (1) could have been expressed explicitly, for instance by the following exchange:

(2) A: Please lend me a pencil. B:

You can use one of my pencilstake one out of my pencil case on the table. In this case, the literal meaning and the intended meaning coincide and no implicature is used in this excerpt. [START_REF] Hagemann | Implikaturanalyse[END_REF] formulates an implicature analysis that refers to Grice's theory of conversation. It follows three steps, which I also use for my analysis: Firstly, contextual elements such as disambiguation and referent assignment have to be determined. Secondly, suspected implicatures have to be tested on cancelability and detachability. Thirdly, a sequence analysis confirms what implicatures are most likely. In example (1) the implicature could be as already suggested above "I need a pencil", but it could also be "I cannot (and I do not want to) write down my solution to the textbook task". The answer of B allows both possible implicatures, but depending on further reactions that may follow this little conversation it can be that one or the other is more plausible. In other words: in the third step you look at what happened before and after the utterance to find out what is most likely intended and understood.

The example

In the following paragraph, I want to demonstrate how I analyze sequences of lessons in order to give a detailed description of what remains implicit in classroom conversation on functions.

The setting of the discussion

Participants in the presented classroom conversation are the members of a course in secondary school with 29 students and their mathematics teacher. The students are in the 11 th grade on a high level, preparing for the last two school years in order to get the Abitur2 . The classroom is equipped with a black board that is used frequently during lessons by the teacher as well as by the students. Tasks are generally handed in in written form on worksheets. The teaching methods and the social forms vary depending on the task. The researcher participates during the lessons only as an observer and does not interfere. The lessons are designed by the teacher without any collaboration with the researcher in order to observe lessons as close as possible to usual lessons.

The task -Walking functions

The task walking functions and the excerpts of the conversation on that task are taken from the first lesson in a unit on functions in the course introduced above. The task walking functions requires transforming a graphic representation of a function into a suitable realistic situation. That means given graphs have to be interpreted. In the setting when a group presents its movements also the reverse is required for the observers: movements have to be referred to graphs. In this task interpretation skills are in the focus while modeling skills only come up to a lesser extend. The transformation of a graph into a movement demands to have a view on the function as a whole and not only on a certain point of the underlying function. In the example above (see Figure 1), the meaning of straight lines, the meaning of the intersections between the graphs with the ordinate as well as meaning of the parallelism of the graphs must be considered. Also the change of distance to the chair in relation to the change of time has to be taken into account.

When having two representations of a function, it is not immediately obvious that those two representations stand for the same function. In this example it can only be seen implicitly by making clear what certain characteristics of a graph mean in the context of the movement in relation to the chair. The second part of the task asks to give an explanation why the group decided on their specific movement. It is asked to make the relation between two representations explicit.

In my analysis of the classroom situation I seek to reconstruct what is made explicit and what remains implicit when an accepted interpretation of the translation from graph into a situation is debated.

The conversation about the task

During the lesson the students worked in groups of three on the task walking functions for about 15 minutes. After working on the task in the groups, three different presentations of movements and explanations were performed. All three groups had different ideas:

In the first group, two students started their movement a few meters away from the chair and walked constantly to the chair. One of them stopped at the chair, the other one stopped at the same time but at some distance to the chair. Their explanation was the following: "Well, we did it that waywell, Paula was the one and Paula started to walk a little earlier because the graph does not start at the zero point. And then Luna came along and then they walked in parallel because they run parallel."3

In the second group, two girls both started in line with the chair and walked vertically to that imaginary line away from the chair keeping the same distance between them. They commented on their movement. A: "Well, not the way that we walk apart, but parallel. But it goes (up) then." B: "[… ] Because we thought that the x-axis is sort of the position of the chair."4

In the third group, two students walked one after another constantly away from the chair. They started and stopped their movement at the same time and explained: "Well, firstly they did not start at the same point because ehm well you have you see on the y-axis that someone starts further ahead, well that he is further away from the chair. […] And they walked at the same speed because the graphs run quasi parallel against each other."5

In the sequence outlined above the students discuss different aspects of the functions in the task. At that point it is not clear which movements and explanations are accepted as a correct translation from the graphic representation into the movement. Subsequently to the presentations, a classroom conversation starts and it is clarified what is considered to be a correct solution to the task. At the end of the discussion, the third group is considered to have presented the best matching movement.

In the following paragraph, I try to reconstruct the process to come to this conclusion and thereby I focus on what remains implicit. The expressions in curly brackets are my interpretation of the intended meaning or rather the implicatures of the utterances.

Finding a suitable movement for the graphs in Figure 1 is not distinct and the different presentations show that the students pick out some characteristics of the graphs and refer them to the movement. All three groups relate the parallelism of the graphs. The first states: "[…] they [the girls] walked in parallel because they [the graphs] run parallel." Presumably they implicate "they [the two girls] walked in parallel because {that is the meaning when} they [the graphs] run parallel." The second group also points out that walking in parallel is the correct transformation: "Well, not the way that we [the two presenting girls] walk apart {by mistake}, but parallel." The third group is the first that relates walking at the same speed to the parallel running graphs: "And they [the two presenting students] walked at the same speed because {that is what is meant when} the graphs run quasi parallel against each other." In all three explanations they mention different characteristics of the functions apart from the parallelism. That is a hint that they see the function as a whole even though not entirely as they miss mentioning some of the functions' relevant characteristics that could be observed in the graphic and situational representation. By their performances and their utterances, the groups made clear what they assume to be the correct relation between the representations. They claim this connection without making explicit why that relation is supposed to be correct.

After these three presentations the teacher asks several questions: "What is the origin of the coordinate system? What is on the x-axis? What is the y-axis? And what does parallel mean?" 6 The teacher seems to pick out the characteristic of the functions she considers to be relevant in this task. When looking at the conversation after these questions you can identify the implicatures: "What is {the meaning of} the origin of the coordinate system {in relation to the situation}? What is {the meaning of} the x-axis {in relation to the situation}? What is {the meaning of} the y-axis {in relation to the situation}? And what does parallel mean {in this context}?" She implicitly focuses the conversation on the relations between the representations. The relations between the representations are discussed for about four minutes. Then the teacher also brings a new possible relation not mentioned before into the discussion: "The graphs go up. That means you walk away from the chair. But it [the movement] is getting faster because {that is meant when} it [the graph] goes up. What do you think of this argument?"7 This utterance brings the students to see the rising of the graph as the speed of the movement and finally to declare that the movements of group three are best matching to the graphs. At no point in the discussion the parallel graphs are related to movements with the same speed again as suggested by group three at the beginning. Although the parallelism is brought into discussion several times the relation between the parallel graphs and the movements with the same speed remains implicit till the end of the conversation sequence about the task walking functions.

Conclusion and discussion

Such a dense description of the activities in the classroom with the focus on the implicit has the aim to make the implicit accessible. can be seen as an objectification of the assumptions and normative demands that resonate subliminally in the lessons. In the presented classroom conversation, the convention that parallel running lines in a path-time diagram stand for movement at the same speed is initiated. This relation between the two representations is declared correct by employing many implicit relations and implicatures. This shows that decoding the implicit in the classroom conversation is relevant. An analysis as demonstrated above can help to understand the demands on teachers and students in the classroom to create and follow lessons sensibly. This analysis of the episode in this paper is just the beginning of my research, my starting point of looking at mathematics lessons with a specific lenswith a lens, which seeks to make invisible demands in mathematics discourse visible. Comparing the analyses of different situations with a similar mathematical content can reveal how the implicit is used in mathematics classroom systematically and give insight into the role of the implicit in teaching and learning of functions. With the help of these analyses I want to develop a local theory on implicitness in classroom talk on functions that links Grice's vast theory of implicatures to the mathematical topic of functions in mathematics classrooms. Whether the evolving theory holds will not be part of this research, but should be probed by using it for broader classroom observations for example.

Didactical implicatures for mathematics lessons deriving from insights in the meaning of the implicit cannot be given at this point of my research. Only as a final result of further analyses ideas for teaching and learning may be devised. For now, I can conclude that implicatures play a role in classroom conversation on functions and that I am curious about finding out more about the relevance of the implicit in mathematical classroom conversation.

Figure 1 :

 1 Figure 1: The taskwalking functions

Proceedings of CERME10

[START_REF] Grice | Logic and conversation[END_REF] maxims of conversation: make your contribution as informative as is required, do not make your contribution more informative than is required, try to make your contribution one that is true, do not say what you believe to be false, do not say that for which your lack adequate evidence, be relevant, be perspicuous, avoid obscurity of expression, avoid ambiguity, be brief, be orderly.Thematic Working Group 09Proceedings of CERME10

The Abitur is the highest graduation in the German school system that forms the general qualification for university entrance.Thematic Working Group 09Proceedings of CERME10

Translated from the German transcript by me. Original: "Also, wir haben die so gemacht weilalso Paula war die eins und Paula ist ein bisschen früher losgelaufen, weil der Graph ja nicht im Nullpunkt startet. Und dann ist Luna mitgekommen und dann sind die parallel gelaufen, weil die parallel verlaufen."

Translated from the German transcript by me. Original: A: "Also so halt nicht, dass wir auseinanderlaufen, sondern parallel. Aber es geht dann (hoch)." B: Weil wir gedacht haben, dass ja die x-Achse sozusagen die Positon vom Stuhl ist. Dann geht das ja davon weg." Thematic Working Group 09 Proceedings of CERME10

Translated from the German transcript by me. Original: "Also erstmal, ähm, sind die Beiden nicht vom gleichen Punkt gestartet, weil ähm, ja weil hat man halt auf der y-Achse sieht, dass jemand weiter vorne startet, also dass er weiter vom Stuhl entfernt ist. Und dann halt so bald neben dem Stuhl. und die sind beide gleich schnell gelaufen, weil die ehm Graphen halt quasi parallel aneinander laufen."

Translated from the German transcript by me. Original: "Was ist der Ursprung des Koordinatensystems? Was ist auf der x-Achse? Was ist auf der y-Achse? Und was heißt das mit dem Parallel?" Thematic Working Group 09 Proceedings of CERME10

Translated from the German transcript by me. Original: "Die Graphen gehen ja hoch. Das heißt, man geht vom Stuhl weg. Aber es wird schneller, weil es ja hoch geht. Was sagt ihr zu diesem Argument?" Thematic Working Group 09 Proceedings of CERME10


Jasmin Christian Blanchette
email: j.c.blanchette@vu.nl

Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)

Keywords: CCS Concepts, Theory of computation → Logic and verification, Automated reasoning, proof systems, theorem provers, proof assistants

IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first-order resolution prover, an imperative SAT solver, and generalized term orders for λ-free higher-order logic.

Introduction

At programming language conferences such as POPL and ICFP, submissions are often accompanied by formalizations. Proof assistants are even used in the classroom to teach language semantics and type systems [START_REF] Nipkow | Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs[END_REF][START_REF] Pierce | Lambda, the Ultimate TA: Using a Proof Assistant to Teach Programming Language Foundations[END_REF].

Paradoxically, the automated reasoning community has largely stood on the sidelines of these developments. Like the shoemaker's children who go barefoot, we reflexively turn to "pen and paper"-by which we usually mean L A T E X-to define our logics, specify our proof systems, and establish their soundness and completeness. The automatic/interactive divide of our community is part of the reason. Few automatic prover developers have first-hand experience with a proof assistant. Nevertheless, it stands to reason that the members of the automated reasoning community should be early adopters of proof assistants. If we cannot convince these close colleagues of the value of tools called "theorem provers, " how are we going to seduce mainstream mathematicians, philosophers, and engineers?

The IsaFoL (Isabelle Formalization of Logic) effort 1 aims at changing this situation. This "coalition of the willing" was inaugurated in 2015, initially as a Bitbucket repository that would enable Mathias Fleury in Saarbrücken and Anders Schlichtkrull in Copenhagen to carry out their respective Ph.D. projects while avoiding duplicated work. Their foresighted and well-funded bosses, Christoph Weidenbach and Jørgen Villadsen, have made this project possible.

My motto for the project is "Coq at POPL, why not Isabelle at CADE?" But in fact, proof assistants, including Isabelle, have been represented at CADE and IJCAR for several years, thanks to Tobias Nipkow, Lawrence Paulson, Christian Urban, and others. Moreover, René Thiemann, Christian Sternagel, and their colleagues have been using Isabelle to formalize term rewriting for over a decade. Their IsaFoR library [START_REF] Thiemann | Certification of Termination Proofs using CeTA[END_REF] directly inspired IsaFoL. 2Our main objective with IsaFoL is to develop libraries and a methodology to support modern research in automated reasoning, especially about propositional and first-order logic. Proof assistants can help when developing proofs, but also when modifying them, to study generalizations and variants. Reviewing becomes much easier when a formalization exists; reviewers can then focus on checking the definitions and theorem statements. Although my primary interest lies in metatheory per se, once we have formal libraries, we can build verified provers and proof checkers on top of them.

The project has grown to include contributions from researchers and students in Amsterdam, Copenhagen, Gothenburg, Grenoble, Munich, Saarbrücken, and Zurich. Contributors include Heiko Becker, Alexander Bentkamp, Andreas Halkjaer From, Alexander Birch Jensen, Peter Lammich, John Bruntse Larsen, Julius Michaelis, Tobias Nipkow, Nicolas Peltier, Andrei Popescu, Simon Robillard, Sophie Tourret, Dmitriy Traytel, and Petar Vukmirović. The IsaFoL repository on Bitbucket is where much of the development takes place. Once individual entries have become mature enough, they tend to migrate to Isabelle's Archive of Formal Proofs, which is continuously tested and updated to work with the most recent version of Isabelle. The maintenance burden largely falls onto the Isabelle developers.

The use of Isabelle/HOL was initially motivated by personal preference, but it has turned out to be a fortunate choice. Isar proofs [START_REF] Wenzel | Isabelle/Isar-a Generic Framework for Human-Readable Proof Documents[END_REF], parameterized modules [START_REF] Ballarin | Locales: A Module System for Mathematical Theories[END_REF], (co)datatypes [START_REF] Biendarra | Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic[END_REF], the code generator [START_REF] Haftmann | Code Generation via Higher-Order Rewrite Systems[END_REF], the Refinement Framework [START_REF] Lammich | Automatic Data Refinement[END_REF], Imperative HOL [START_REF] Bulwahn | Imperative Functional Programming with Isabelle/HOL[END_REF], and the Sledgehammer [START_REF] Paulson | Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers[END_REF] and Nitpick [START_REF] Tiwari | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder[END_REF] tools have all played important roles. Higher-order logic's lack of expressiveness is often cited as a drawback of the system, but it has not been an issue for me in this project. Using Isabelle has been an opportunity to "eat my own dog food, " gaining insights into how the subsystems I am responsible for-the (co)datatypes, Sledgehammer, and Nitpick-could be improved.

In his invited SAS 2018 paper [START_REF] O'hearn | Experience Developing and Deploying Concurrency Analysis at Facebook[END_REF], Peter O'Hearn put forward the notion that in most research papers one gets a description of where a project got to, but not how it got there. We get the results of science and/or engineering, but not a picture of how it developed. For the practice of doing science and engineering I've always thought the issue of "how it's done" is an important one.

In this spirit, I describe three subprojects of IsaFoL to which I have contributed: a first-order prover based on ordered resolution (Section 2), an optimized SAT solver based on conflict-driven clause learning (Section 3), and generalized term orders for λ-free higher-order logic (Section 4). I reflect on the motivation and rewards of such work, both scientific and metascientific, and use this opportunity to survey related work, including the other IsaFoL entries (Section 5).

All along, my primary metascientific motivation has been to continue carrying out research at the intersection of interactive and automatic proving, enabling me to remain in the CADE orbit. After the Sledgehammer success storyautomatic provers at the service of interactive ones [START_REF] Paulson | Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers[END_REF]-I was stimulated by the thought of reversing the formula. There is an undeniable self-referential thrill to the project.

Formalize logic in logic. Employ automatic provers to formalize their own metatheory. But as the project advanced, I started to appreciate its deeper value. The overwhelmingly positive response at CADE, CPP, IJCAR, and JAR has convinced me that this research program was overdue.

I am excited about recent developments, where flaws and limitations revealed in formalization motivate new research. We are gradually moving from carrying out case studies, where the proof assistant aspect is predominant, to writing metatheory papers that only briefly mention the formal development in their introduction.

A First-Order Ordered Resolution Prover

Nearly two decades after its publication, the Handbook of Automated Reasoning [START_REF]Handbook of Automated Reasoning[END_REF] remains an invaluable resource for researchers in the area. In 2014, I started formalizing its Chapter 2, written by Bachmair and Ganzinger [START_REF] Bachmair | Resolution Theorem Proving[END_REF]. The first four sections present the metatheory of ordered resolution with selection, culminating in Section 4.3 with a refutationally complete first-order prover, RP, based on this calculus. At the time, I had little experience using Isabelle, so it was fortunate that Traytel agreed to act as my mentor.

The chapter had been haunting me as a tsundoku for a couple of years. Formalizing it meant I would finally have to take it from my reading pile and read it thoroughly. But there were also sound scientific reasons to choose this target for formalization, as we remarked later [89, Section 1]:

The text is a standard introduction to superposition-like calculi (together with Handbook Chapters 7 and 27). It offers perhaps the most detailed treatment of the lifting of a resolution-style calculus's static completeness to a saturation prover's dynamic completeness. It introduces a considerable amount of general infrastructure, including different types of inference systems (sound, reductive, counterexample-reducing, etc.), theorem proving processes, and an abstract notion of redundancy. The resolution calculus, extended with a term order and literal selection, captures most of the insights underlying ordered paramodulation and superposition.

Traytel and I made quick progress in two intense weeks, reaching the crucial Section 4.3. This is where the resolution calculus is lifted from ground (propositional) to nonground (first-order) clausal logic and where the RP prover is introduced and shown to be refutationally complete.

At the ground level, ordered resolution consists of the single (n + 1)-ary inference rule

C i ∨ A i ∨ • • • ∨ A i n i=1 ¬ A 1 ∨ • • • ∨ ¬ A n ∨ D C 1 ∨ • • • ∨ C n ∨ D
with multiple side conditions that restrict the search space. This rule is refutationally complete, meaning that any unsatisfiable set that is closed under applications of the rule will contain the empty clause ⊥. Remarkably, replacing the Formalizing the Metatheory of Calculi and Provers CPP '19, January 14-15, 2019, Cascais, Portugal subclause A i ∨ • • • ∨ A i with a single literal A i is enough to make the rule incomplete [START_REF] Bachmair | Resolution Theorem Proving[END_REF].

A redundancy criterion identifies clauses and inferences that can be ignored. For example, p(a) ∨ q(b) is made redundant by p(a), which in turn is made redundant by p(x).

Next, Bachmair and Ganzinger introduce the concept of a theorem proving process: a transition system that starts with an initial clause set N 0 and where each transition ▷ corresponds either to an inference or the removal of redundant clauses. Under a fairness assumption, the calculus's completeness theorem characterizes the limit of a derivation

N 0 ▷ N 1 ▷ N 2 ▷ • • • .
Section 4.3 is where the trouble starts. For nonground clauses, the resolution rule takes the form

C i ∨ A i1 ∨ • • • ∨ A ik i n i=1 ¬ A 1 ∨ • • • ∨ ¬ A n ∨ D (C 1 ∨ • • • ∨ C n ∨ D)σ
where σ is the most general unifier of the set of constraints

{A i1 ? = • • • ? = A ik i ? = A i | i ∈ {1, .
. . , n}}. Side conditions block inferences where A i σ is smaller than C i σ or Dσ with respect to a fixed order. A literal selection mechanism further prunes the search space.

Traytel and I initially stopped here. By a stroke of good fortune, Schlichtkrull decided to resume the proof two years later. After months of labor, and with expert help from Waldmann, he reached the final qed. The resulting IJCAR 2018 paper [START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] was well received by the reviewers, reaping a "strong accept" and two "accepts. " One of them wrote:

The authors convinced me that their development is a great tool for exploring/developing calculus extensions. It will enable us to "extend/hack without fear. " (The italics are mine throughout this paper.)

The RP prover is naturally formulated in Isabelle as an inductive predicate. Bachmair and Ganzinger's transition rules correspond directly to introduction rules: inductive :: ′ a state ⇒ ′ a state ⇒ bool where tautology_delete:

Neg A ∈ C ∧ Pos A ∈ C =⇒ (N ∪ {C}, P, O) (N , P, O) | forward_subsume: D ∈ P ∪ O ∧ subsumes D C =⇒ (N ∪ {C}, P, O) (N , P, O) | backward_subsume_P: D ∈ N ∧ ssubsumes D C =⇒ (N , P ∪ {C}, O) (N , P, O) | backward_subsume_O: D ∈ N ∧ ssubsumes D C =⇒ (N , P, O ∪ {C}) (N , P, O) | forward_reduce: D ∈ P ∪ O ∧ reduces D C L =⇒ (N ∪ {C ⊎ {L}}, P, O) (N ∪ {C}, P, O) | backward_reduce_P: D ∈ N ∧ reduces D C L =⇒ (N , P ∪ {C ⊎ {L}}, O) (N , P ∪ {C}, O) | backward_reduce_O: D ∈ N ∧ reduces D C L =⇒ (N , P, O ∪ {C ⊎ {L}}) (N , P ∪ {C}, O) | clause_process: (N ∪ {C}, P, O) (N , P ∪ {C}, O) | inference_compute: (∅, P ∪ {C}, O) (concl_of ' infers_between O C, P, O ∪ {C})
We faced various difficulties when formalizing Section 4.3. It did not help that the text contains dozens of small mistakes. Even the statement of the nonground resolution rule suffers from typos and ambiguities. While we agree with the reviewer who wrote that "most of us unconsciously autocorrect it, and read it with the intended meaning, " on several occasions we found ourselves blindly trusting the text, only to be disappointed later.

Reasoning about the (n + 1)-premise resolution rule was particularly tedious. Ellipsis is a convenient pen-and-paper device that lacks a counterpart in proof assistants. We ended up keeping the clauses C i and atoms A i = {A i1 , . . . , A ik i } in parallel lists. Ideally, the first n premises of the rule would be regarded as a multiset; there is no need to consider n! inferences all yielding the same clause. However, there is no such things as "parallel multisets," and our attempts at storing tuples (C i , A i ) in multisets only made matters worse.

Another general difficulty with the chapter was that it is not always clear which hypotheses apply where. The text both presents a general framework and applies it, but dependencies are not tracked precisely, and many lemmas are never invoked explicitly. It was a challenge to understand the informal proof well enough to organize the modules and state the definitions and lemmas precisely and correctly.

Finally, some of the arguments are incomplete or misleading. The proof of Lemma 4.11 relies on the observation that "D ′ cannot be deleted by backward reduction or backward subsumption. " However, in principle, D ′ could be deleted due to the presence of a more general clause D ′′ , which in turn could be deleted due to D ′′′ , and so on. The key missing observation is that this process can be iterated at most finitely many times, generalization being a well-founded relation.

With the module hierarchy, definitions, and key lemma statements in place, carrying out the proofs was mostly straightforward. We relied heavily on Sledgehammer to discharge the proof obligations.

We did find a significant mistake in the chapter. Theorem 4.13 states that RP is refutationally complete, but this does not hold due to the improper treatment of inferences containing duplicate premises. Remarkably, we discovered the mistake several months after reaching the final qed, while reviewing our definitions. We had inadvertently "autocorrected" Bachmair and Ganzinger's definition of RP.

Formalization helps track assumptions and dependencies precisely. It helps us answer questions such as, "Is Lemma 3.13 actually needed, and if so, where?" Indeed, such a question recently arose in the course of Bentkamp's research on superposition [START_REF] Bentkamp | Superposition for Lambda-Free Higher-Order Logic[END_REF]. He wanted to understand why the literal selection function S M is defined so that "(ii) S M (C) = S(C), if C is not in K. " He quickly got two replies. Waldmann wrote:

As far as I can see, S M is really only needed for ground instances, and then case (ii) is irrelevant. I guess they just wanted to define S M as a total function. Thanks to Isabelle, Schlichtkrull could be more confident:

I tried to change the definition in the formalization to return the empty multiset if C is not in K. With this definition the above properties also hold, and the proof goes through. This anecdote nicely illustrates how formal proofs help generate knowledge and understanding. Here, they helped Bentkamp "extend/hack without fear. "

The second half of Bachmair and Ganzinger's chapter, starting with Section 5, focuses on variations, such as nonstandard clauses and hyperresolution. Most of these are not implemented in modern provers, and we did not attempt to formalize this material. Instead, Schlichtkrull, Traytel, and I further refined the abstract prover RP to obtain an executable functional program. This work is described in a paper included in these proceedings [START_REF] Schlichtkrull | A Verified Prover Based on Ordered Resolution[END_REF].

We started by defining the inductive predicate RP w , which resembles RP but adds a timestamp to clauses and a weight function. Bachmair and Ganzinger [3,p. 44] mention this idea in a footnote, but they require the weight function to be monotone in both the timestamp and the clause size, claiming that this is necessary to ensure fairness. Although it often makes sense to prefer smaller clauses, our proof reveals that this is not necessary to ensure fairness.

Next, we defined RP d as a deterministic functional program. RP d simply calls the auxiliary function RP d _step repeatedly until a final state (with N = P = ∅) is reached. RP d _step is a function of about 40 lines of code that is loosely modeled after Vampire's main loop [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF]. To introduce this possibly nonterminating function in Isabelle, we defined RP d by means of an option monad, using the partial_function command [START_REF] Krauss | Recursive Definitions of Monadic Functions[END_REF], so that it returns a value of the form Some R if the computation terminates and None otherwise.

Finally, we made RP d executable by connecting it to IsaFoR, which provides first-order terms [START_REF] Sternagel | First-Order Terms[END_REF] and operations on them, such as unification and the Knuth-Bendix order. We invoked Isabelle's code generator [START_REF] Haftmann | Code Generation via Higher-Order Rewrite Systems[END_REF] to export the prover to Standard ML. The resulting program, RP x , consists of about 1000 lines of functional ML code, including dependencies.

After working hard to obtain an executable prover, we evaluated it on a representative subset of 1000 TPTP benchmarks against two leading provers, E [START_REF] Schulz | E-a Brainiac Theorem Prover[END_REF] and Vampire [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF], as well as Metis [START_REF] Hurd | First-Order Proof Tactics in Higher-Order Logic Theorem Provers[END_REF], which is written in Standard ML. The table below gives the number of problems solved (proved or disproved) by each prover [START_REF] Schlichtkrull | A Verified Prover Based on Ordered Resolution[END_REF]:

Vampire E Metis RP x 833 770 527 353
Although our prover cannot yet challenge the state of the art, its performance is respectable and could be improved further using refinement. In his presentations, Natarajan Shankar often stresses the view that algorithm = inference + strategy + indexing Indeed, the performance of an automatic proof procedure comes largely from three sources: the calculus, the heuristics, and the data structures. RP x implements an excellent calculus, but mediocre heuristics and data structures. In the next section, we will look at a verification project that takes these two aspects seriously. The work on formalizing RP and RP x opens exciting perspectives. First, it paves the way for the formalization of superposition-based provers. Peltier [START_REF] Peltier | A Variant of the Superposition Calculus[END_REF] took us by surprise when he announced, in 2016, his Isabelle formalization of the superposition calculus. Based on his work, it should be possible to define an SP prover analogous to RP, but which could reason efficiently about equality, implementing most of the simplification rules and heuristics described in, for example, the E paper [START_REF] Schulz | E-a Brainiac Theorem Prover[END_REF]. Verifying data structures such as discrimination trees, feature-vector indices, and fingerprint indices would pose interesting challenges. In unpublished work, Vukmirović has verified the underlying principles of fingerprints [START_REF] Schulz | Fingerprint Indexing for Paramodulation and Rewriting[END_REF] for λ-free higher-order logic [START_REF] Vukmirović | Extending a Brainiac Prover to Lambda-Free Higher-Order Logic[END_REF] using Isabelle.

Another perspective is to improve Bachmair and Ganzinger's framework. In unpublished work, Waldmann, Tourret, Robillard, and I have conceived, with pen and paper, a framework that captures abstractly the lifting from a ground calculus's completeness result to a nonground RP-like prover. An Isabelle formalization is underway, which should culminate with a streamlined proof of Bachmair and Ganzinger's Theorem 4.13. The framework will also support infinitary inferences; these are useful for automating higher-order logic, where the unification procedure may yield an infinite stream of incomparable unifiers.

Around 2012, Vampire was extended with a SAT solver, using a novel architecture called AVATAR [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF]. The empirical results were sensational, but a fundamental question was left unanswered: is AVATAR refutationally complete? The literature contains contradictory, erroneous definitions of the architecture [START_REF] Bjø | [END_REF][START_REF] Reger | Playing with AVATAR[END_REF][START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF], but following discussions with Giles Reger and his colleagues, I believe I have reached a precise definition, for which refutational completeness holds, while isolating a few potential sources of incompleteness in Vampire. Furthermore, Vukmirović and I have shown that labeled splitting [START_REF] Fietzke | Labelled Splitting[END_REF], as implemented in SPASS, can be seen as an instance of a slightly generalized AVATAR. I hope to establish all of this formally in Isabelle, using the new framework by Waldmann et al. described above.

Inconveniently for us, there already existed several verified CDCL-based solvers [START_REF] Lescuyer | Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq[END_REF][START_REF] Marić | Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL[END_REF][START_REF] Marić | Formalization of Abstract State Transition Systems for SAT[END_REF][START_REF] Oe | versat: A Verified Modern SAT Solver[END_REF][START_REF] Shankar | The Mechanical Verification of a DPLL-Based Satisfiability Solver[END_REF]. We found a niche by emphasizing the stepwise refinement methodology and the connection between calculi variants, and by considering some aspects that had not been the focus of formalization before: clause forgetting, solver restarts, and incremental solving. We hoped this would suffice to get our submission accepted at IJCAR 2016; little did we expect to receive the best paper award. In the jury's words, our paper [START_REF] Christian Blanchette | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF] formalizes a modern SAT solver via a chain of refinements in a proof assistant, contributing to the program of formalizing highly-technical research in the field of automated reasoning using tools developed in this field.

We considered both the abstract CDCL calculus described by Nieuwenhuis, Oliveras, and Tinelli [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T )[END_REF] and a refined implementation-oriented calculus proposed by Weidenbach [START_REF] Weidenbach | Automated Reasoning Building Blocks[END_REF]. The calculi are represented by inductive predicates on state tuples, roughly along the lines of the RP prover described in the previous section.

The proofs are largely elementary, relying on basic results about multisets and well-founded relations. We generally found Nieuwenhuis et al.'s arguments easy to follow, with the notable exception of a gap in their termination proof. Weidenbach's concise proofs were often more challenging to formalize. To give a flavor of his text, I quote a passage that argues why it is impossible for the same clause to be derived, or "learned, " twice: By contradiction. Assume CDCL learns the same clause twice, i.e., it reaches a state (M, N , U , D ∨ L) where Jump is applicable and D ∨ L ∈ N ⊎ U . More precisely, the state has the form

(K n • • • K 2 K † 1 M 2 K † M 1 , N , U , D ∨ L)
where the K i , i > 1 are propagated literals that do not occur complemented in D, as otherwise D cannot be of level i. Furthermore, one of the K i is the complement of L. But now, because

D ∨ L is false in K n • • • K 2 K † 1 M 2 K † M 1 and D ∨ L ∈ N ⊎ U instead of deciding K †
1 the literal L should be propagated by a reasonable strategy. A contradiction. Note that none of the K i can be annotated with D ∨ L. Fleury needed over 700 lines of Isabelle to capture this paragraph. By changing the argument, he was later able to reduce the formal proof down to 250 lines. The key was to exploit invariance: by first establishing a strong invariant on SAT solver states (namely, that all unit propagations have been performed before deciding a new literal), he could easily perform the key step of the argument ("the literal L should be propagated by a reasonable strategy") without having to refer to earlier states or transitions.

Although Fleury did not discover any significant flaw in the metatheory of CDCL (which would have been most surprising), he did find a critical mistake in an extension, described in Weidenbach's draft, of CDCL with the branchand-bound principle. He came up with a counterexample that invalidates the main correctness theorem, whose proof confused partial and total models. Interestingly, he later noticed the same flaw in a SAT 2009 paper by Larrosa et al. [START_REF] Larrosa | Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates[END_REF]; the issue is silently repaired in a subsequent article [START_REF] Larrosa | A Framework for Certified Boolean Branch-and-Bound Optimization[END_REF].

As a proof of concept, Fleury implemented a deterministic SAT solver and extracted functional Standard ML code from it, preserving the formal guarantees established about CDCL: soundness, completeness, and termination. The resulting program was very inefficient; it could solve none of the 2009 SAT Competition problems in reasonable time.

This was good enough for me but not for Fleury. With Lammich's help, he proceeded to specify the two-watchedliteral (2WL) scheme and other imperative data structures [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF], gradually departing from Weidenbach's draft. This work is described in a JAR article [START_REF] Christian Blanchette | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF] and a CPP 2018 paper [START_REF] Fleury | A Verified SAT Solver with Watched Literals using Imperative HOL[END_REF].

The 2WL scheme makes it possible to efficiently identify candidate clauses for unit propagation and conflict detection, which are the core CDCL operations. In each clause, the solver distinguishes two watched literals-literals that can possibly influence their clauses' truth value in the solver's current state. The solver maintains the "2WL invariant" for each clause. Unfortunately, the literature is imprecise about the nature of this invariant and about when it is required to hold. Fleury quickly found himself studying MiniSat's source code [START_REF] Eén | An Extensible SAT-Solver[END_REF], and eventually came up with a precise formulation. He specified 2WL as an abstract calculus, following Weidenbach's draft, and proved that its transitions preserve the 2WL invariant. To get an executable program, he refined the calculus in several correctness-preserving steps. The refinement methodology enabled him to inherit invariants, correctness, and termination from previous layers.

The next refinement step implements the rules of the 2WL calculus in a more algorithmic fashion, using the nondeterministic programming language provided by Lammich's Refinement Framework [START_REF] Lammich | Automatic Data Refinement[END_REF]. The language is built on top of a nondeterminism monad. To give a flavor of it, I present the code of a function that implements four calculus rules:

definition PCUI algo :: ′ v lit × ′ v clause → state → state where PCUI algo LC S = do { let (M, N , U , D, NP, UP, WS, Q) = S; let (L, C) = LC; L ′ ← RES {L ′ | L ′ ∈ watched C -{L}}; if L ′ ∈ M then RETURN S else if ∀L ∈ unwatched C. -L ∈ M then if -L ′ ∈ M then RETURN (M, N , U , C, NP, UP, ∅, ∅) else RETURN (L ′C • M, N , U , D, NP, UP, WS, {-L ′ } ⊎ Q) else do { K ← RES {K | K ∈ unwatched C ∧ -K M }; (N ′ , U ′ ) ← RES {(N ′ , U ′ ) | update_clss (N , U ) C L K (N ′ , U ′ )}; RETURN (M, N ′ , U ′ , D, NP, UP, WS, Q) } }
The subsequent refinement steps optimize the data structures and specify heuristics that reduce the nondeterminism, following ideas from the SAT literature and actual implementations. Multisets give way to lists, and clauses are now referenced by indices into a list of clauses instead of stored directly. For each literal L, the clauses that contain a watched L are chained together in a linked list, called a watch list.

The Sepref tool [START_REF] Lammich | Refinement to Imperative/HOL[END_REF], which is based on separation logic, can be used to synthesize imperative code from a monadic Isabelle program. It replaces the functional data structures by imperative implementations, while leaving the algorithmic structure unchanged. The resulting program, called IsaSAT, is expressed using Imperative HOL's heap monad [START_REF] Bulwahn | Imperative Functional Programming with Isabelle/HOL[END_REF]. Using Isabelle's code generator [START_REF] Haftmann | Code Generation via Higher-Order Rewrite Systems[END_REF], we can extract a self-contained program in imperative Standard ML.

Since the CPP 2018 publication, Fleury has improved Isa-SAT further by implementing four optimizations: restarts, forgetting, blocking literals, and machine integers.

Restarts is a technique that enables the solver to explore another part of the search space. We can keep completeness by gradually increasing the interval between restarts. Our calculi included an optional Restart rule all along to allow such behavior, but it was not implemented in the first IsaSAT.

Forgetting removes some learned clauses-consequences of the initial problem clauses that are derived during solving. Helpfully, the abstract CDCL calculus included a Forget rule from the start. The main difficulty is that each clause now needs to store a Boolean flag indicating whether it is deleted. This requires adding a header to the clause data structure for storing this and other useful information that guides the heuristics, and adapting all the refinement proofs.

Blocking literals are literals stored directly in the watch list, next to a pointer (or index) to the clause, that can be checked directly without dereferencing the pointer. The information is redundant, but it often saves a pointer dereference.

Machine (64-bit) integers are large enough to store clause indices and other numbers for all SAT problems arising in practice, and they are more efficient than ML's unbounded integers. To use them without losing the formal guarantees about the program, we generate two versions of the prover's body and connect them with code of the form while ¬ done ∧ ¬ overflow do ⟨invoke the 64-bit version of the solver's body⟩;

if ¬ done then ⟨convert the state from 64-bit to unbounded integers⟩; while ¬ done do ⟨invoke the unbounded version of the solver's body⟩

In a preliminary evaluation, Fleury ran IsaSAT against four other solvers on a collection of 3313 benchmark problems, consisting of all the SAT Competition problems from the 2009, 2011, 2013, 2014, 2016, and 2017 editions of the SAT Competition and the 2015 edition of the SAT-Race. The solvers Glucose [START_REF] Audemard | Predicting Learnt Clauses Quality in Modern SAT Solvers[END_REF] and CaDiCaL [START_REF] Biere | CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition[END_REF] represent the state of the art; MiniSat [START_REF] Eén | An Extensible SAT-Solver[END_REF] is a well-known reference solver; and versat [START_REF] Oe | versat: A Verified Modern SAT Solver[END_REF] is the only other efficient verified solver we know of. Since IsaSAT does not implement preprocessing techniques yet, CryptoMiniSat [START_REF] Soos | Extending SAT Solvers to Cryptographic Problems[END_REF] was used to simplify all problems before benchmarking. The tests were run with a time limit of [START_REF] Dershowitz | Proving Termination with Multiset Orderings[END_REF] Given that competitive SAT solvers are extremely optimized programs, these results are very encouraging. However, we must bear in mind that it took two years of hard labor, and tens of thousands of Isabelle lines, to get from 0 to 731. An obvious avenue for future work would be to add optimizations such as pre-and inprocessing [START_REF] Järvisalo | Inprocessing Rules[END_REF]. A benefit of having a verified SAT solver is that it can be employed as a backend in other verified tools. We have started looking into extending IsaSAT with theory reasoning, as in an SMT (satisfiability-modulo-theories) solver, with the goal of integrating it in CeTA [START_REF] Brockschmidt | Analyzing Program Termination and Complexity Automatically with AProVE[END_REF], a verified safety and termination proof checker developed as part of IsaFoR.

Lambda-Free Higher-Order Terms Orders

The last subproject has a different flavor from the other two, in that the formalization arose as a side effect of carrying out research in automated reasoning and not as an end in itself. The Matryoshka project, 3 which started in 2017 and funds a collaboration between Amsterdam, Nancy, Saarbrücken, and Stuttgart, aims at extending superposition provers and SMT solvers with higher-order features. As a stepping stone towards full higher-order logic, we started by focusing on a λ-free fragment. Unlike in first-order logic, variables may be applied, and function symbols may be given fewer arguments than they can take. This language is sometimes called "applicative first-order" in the term-rewriting community.

Bentkamp developed, under Waldmann's and my supervision, a refutationally complete superposition calculus for λ-free higher-order logic and implemented it in a prototype prover developed with Cruanes [START_REF] Bentkamp | Superposition for Lambda-Free Higher-Order Logic[END_REF]. He wrote his proofs directly in L A T E X, which was possible only because he is extremely rigorous and could count on two experts to check his proofs-namely, Waldmann and our colleague Tourret. In principle, he could have started from Peltier's Isabelle formalization of superposition [START_REF] Peltier | A Variant of the Superposition Calculus[END_REF], but it seemed more difficult than working in L A T E X, especially given that he was more familiar with Waldmann's informal proof, which has a different structure from Peltier's.

Superposition, like ordered resolution (Section 2), relies on a well-founded term order. Together with Becker, Waldmann, and Wand, I designed two (families of) orders that generalize the familiar Knuth-Bendix order (KBO) and recursive path order (RPO). Becker formalized most of KBO during an internship; I completed his work and proceeded with RPO. This research was presented at FoSSaCS 2017 [START_REF] Christian Blanchette | A Lambda-Free Higher-Order Recursive Path Order[END_REF] and CADE 2017 [START_REF] Becker | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms[END_REF].

The term orders are comparatively simple mathematical objects that lend themselves well to mechanization. I worked directly in Isabelle to define them and state their desired properties, starting with the ground case. The following fragment corresponds to my first attempt at defining a lexicographic path order (LPO), a special case of RPO, on ground terms:

datatype ′ c tm = F ′ c ( ′ c tm list) context fixes ≺ c :: ′ c ⇒ ′ c ⇒ bool assumes irreflp (≺ c ) and transp (≺ c ) and f ≺ c д ∨ д ≺ c f ∨ f = д begin definition chksubs :: ( ′ c tm ⇒ ′ c tm ⇒ bool) where chksubs R s t ←→ (case (s, t) of (F f ss, F д ts) ⇒ (∀s ′ ∈ ss. R s ′ t ∨ s ′ = t) ∧ (ss [] ∧ ts [] ∧ last ss = last ts -→ R (F f (butlast ss)) (F д (butlast ts)))) inductive ≺ :: ′ c tm ⇒ ′ c tm ⇒ bool where s ≺ t ∨ s = t =⇒ s ≺ F f (ts @ [t])) | s = F f ss ∧ t = F д ts ∧ s ≺ t =⇒ F f (ss @ [u]) ≺ F д (ts @ [u]) | s = F f ss ∧ t = F д ts ∧ f ≺ c д ∧ chksubs (≺) s t =⇒ s ≺ t | s = F f ss ∧ t = F f ts ∧ chksubs (≺) s t ∧ lexordp (≺) ss ts =⇒ s ≺ t lemma irrefl: ¬ s ≺ s lemma trans: s ≺ t ∧ t ≺ u =⇒ s ≺ u lemma total: s ≺ t ∨ t ≺ s ∨ s = t lemma compat_fun: s ≺ t =⇒ F f (ss @ s • ss ′ ) ≺ F f (ss @ t • ss ′ ) lemma compat_arg: F f ss ≺ F д ts =⇒ F f (ss @ [s]) ≺ F д (ts @ [s]) . . . end
The specification is very short and depends on no background theory beyond list operations (cons •, append @, butlast, lexordp). It is a perfect match for my counterexample generator Nitpick [START_REF] Tiwari | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder[END_REF]. And indeed, the tool quickly finds a counterexample to the irrefl conjecture: given a type ′ c with two distinct symbols f, g such that f ≺ c g, we have f (g f) ≺ f (g f). (Sadly, Nitpick's rival Quickcheck [START_REF] Bulwahn | The New Quickcheck for Isabelle: Random, Exhaustive and Symbolic Testing under One Roof[END_REF] fails with the error "No type arity tm :: full_exhaustive. ") Using Nitpick, I was able to converge to an almost correct design. A major flaw had escaped my attention, namely: without arities or typing constraints, LPO is not well founded, because it allows infinite descending chains such as

f b ≻ f a b ≻ f a a b ≻ f a a a b ≻ • • •
This was noticed early on by Waldmann. Nitpick is helpless here, because it is based on finite model finding. It can be used to detect cycles but not acyclic divergence.

For the proofs, we drew our inspiration mostly from Baader and Nipkow's textbook [START_REF] Baader | Term Rewriting and All That[END_REF]. However, they cover only LPO and not RPO. When formalizing RPO, I faced a chicken-andegg problem that took me several days to untangle. The issue is related to the multiset order, which is used to define RPO. There exist two main formulations of the multiset order: Dershowitz-Manna [START_REF] Dershowitz | Proving Termination with Multiset Orderings[END_REF] and Huet-Oppen [START_REF] Huet | Equations and Rewrite Rules: A Survey[END_REF]. They are equivalent on partial orders. Since RPO is a partial order, at first I chose Huet-Oppen, which we had used for KBO; however, until we have proved irreflexivity and transitivity of RPO, we cannot assume it is a partial order, so the choice between the two multiset orders is crucial. Zantema [START_REF] Zantema | Termination[END_REF] was well aware of this, but I came across his work too late. And regardless, I could not think clearly while under the charm of the myth "Dershowitz-Manna = Huet-Oppen. "

As is often the case, once the main ideas were clarified, the formal proofs were straightforward to develop. According to generated logs, on some days I invoked Sledgehammer over 100 times. The first-order nature of most proof obligations (with the notable exception of well-foundedness) was a good match for automatic provers. The following Isar fragment, where each subproof (highlighted in gray) was produced by Sledgehammer, is fairly representative: have arity_hd (head s) = 1 by (metis One_nat_def arity.wary_AppE dual_order.order_iff_strict eSuc_enat enat_defs(1,2) ileI1 linorder_not_le not_iless0 wary_st wt_gt_δ _if_superunary wt_s) hence nargs_s: num_args s = 0 by (metis enat_ord_simps(2) less_one nargs_lt one_enat_def ) have s = Hd (head s) by (simp add: Hd_head_id nargs_s) then obtain f where f ∈ ground_heads (head s) and wt_sym f + the_enat (δ * arity_sym f ) = δ using exists_wt_sym wt_s by fastforce

The first proof above relies on 12 lemmas. Developing such a proof manually could easily have taken half an hour without the help of Sledgehammer (to find the proof) or the metis proof method (to reconstruct it), and would have required searching for lemmas or memorizing their names.

In our two papers and the associated technical reports, we presented informal versions of the Isabelle proofs, for human consumption. This has been an opportunity to clean up and restructure the Isabelle proofs, to emphasize the important steps. We also used Nitpick to create examples to illustrate fine points in the papers [START_REF] Becker | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms[END_REF]Example 12;[START_REF] Christian Blanchette | A Lambda-Free Higher-Order Recursive Path Order[END_REF]Example 9]. Given two orders ≺ 1 and ≺ 2 , we could ask the tool to generate terms s, t such that s ≺ 1 t but s ≻ 2 t.

Proof assistants really come into their own when we start modifying existing developments. Late in the project, we asked ourselves, "Could we generalize definition so-and-so in such-and-such a way?" After spending one hour with Isabelle, I was convinced the answer was yes, and a few hours later I was done repairing the proofs. There was very little to change in the technical report, but I would have had a hard time locating the passages that needed modifications and convincing myself that I had found them all.

The two papers received a lukewarm welcome. The term orders were not implemented in any termination tool, nor (at the time) in a superposition prover, and some related work was not treated. Nevertheless, the reviewers were ostensibly impressed by the formalization, which probably saved the submissions. I realize I may be preaching to the choir, but let me quote two of the reviews:

Statements are very precise. Only necessary conditions are made. In particular, orders are characterized by 9 properties, and for each main statement, the authors discuss which of them are necessary.

[The submission] incorporates a comprehensible structure, precise assumptions and thorough proofs for all the KBO's essential properties. All the presented proofs (irreflexivity, transitivity, subterm property, compatibility with functions and arguments, stability under substitution, totality on ground terms, well-foundedness) have been formalized within Isabelle/HOL and published as part of the Archive of Formal Proofs. Together with the careful presentation of these proofs within the submission, this establishes a high overall reliability of the presented results.

Isabelle helped in other ways during the CADE rebuttal phase. A reviewer had asked, "Doesn't X2 follow from X1 by taking x ≻ 2 y iff h(x) ≻ 1 h(y)?" Using Nitpick, we were able to provide a simple counterexample.

Our λ-free higher-order RPO suffers for a theoretical blemish: it does not satisfy compatibility with arguments, the requirement that s ≺ t implies s u ≺ t u for all terms s, t, u. In fact, this requirement cannot be met while maintaining the subterm property and coincidence with the standard RPO on the first-order fragment of higher-order terms. In 2017, I challenged Bentkamp to design an RPO-like order that satisfies compatibility with arguments, by giving up full coincidence with the standard RPO. He succeeded brilliantly. He even used Isabelle to design his new order, the embedding path order (EPO) [START_REF] Bentkamp | Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms[END_REF], and reports that proving the properties formally was easier than it would have been with pen and paper. On the other hand, he struggled with my tool Nitpick and ended up testing his conjectures by coding them in Haskell and using Lazy SmallCheck [START_REF] Runciman | SmallCheck and Lazy SmallCheck: Automatic Exhaustive Testing for Small Values[END_REF].

At some point, I generalized our definition of KBO to use ordinals instead of natural numbers, resulting in a transfinite KBO (TKBO). For this work, I collaborated with Fleury and Traytel. Using Isabelle's new (co)datatype package [START_REF] Biendarra | Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic[END_REF], we could define the syntactic ordinals -the ordinals below ϵ 0 , representable in Cantor normal form-as the following datatype of hereditarily finite multisets:

datatype hmultiset = HMSet (hmultiset multiset) The recursion through a nondatatype, multiset, would be problematic in other systems, or in pre-2013 versions of Isabelle/HOL. An ordinal α = ω

α 1 • c 1 + • • • + ω α n • c n in
Cantor normal form is identified with the hereditarily finite multiset

α = { c 1 copies α 1 , . . . , α 1 , . . . , c n copies α n , . . . , α n }
We used this opportunity to also introduce a type of nested finite multisets and defined Dershowitz and Manna's nested multiset order on it [START_REF] Dershowitz | Proving Termination with Multiset Orderings[END_REF]:

datatype ′ a nmultiset = Elem ′ a | MSet ( ′ a nmultiset multiset)
This enabled us to finally give a positive answer to Paulson, who in 2014 had asked on the Isabelle mailing list: I wonder whether anybody is aware of a formalisation (in any system) of the nested multiset ordering, as described in the classic paper "Proving Termination With Multiset Orderings"? Using Isabelle's Lifting and Transfer tools [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF], we established a bijection between hmultiset and the Elem-free fragment of ′ a nmultiset and exploited it to lift definitions and properties. Notably, lifting the nested multiset order gives the familiar < operator on ordinals. The order's wellfoundedness proof can be transferred as well. Ordinal arithmetic operations such as addition and multiplication can be defined directly in terms of multiset operations.

Overall, we were able to quickly develop a versatile, practical library of syntactic ordinals, which we used not only for our TKBO variant but also in a formal proof of Goodstein's theorem. This research was presented at FSCD 2017 [START_REF] Christian Blanchette | Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL[END_REF].

Related Work

IsaFoL consists of many more subprojects beyond those described above. The first two listed below predate IsaFoL, but they are very much in its spirit and are mentioned on its web page. The entries are listed in rough chronological order:

• equisatisfiability of sort encodings for first-order logic, by Popescu and myself [START_REF] Paulson | Mechanizing the Metatheory of Sledgehammer[END_REF][START_REF] Schmidt | Sound and Complete Sort Encodings for First-Order Logic[END_REF] [START_REF] Ridge | A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic[END_REF][START_REF] Ridge | A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic[END_REF] of a sequent calculus for a term-free first-order logic, by Villadsen, Schlichtkrull, and From [START_REF] Villadsen | Simple Prover. Isabelle Formalization of Logic[END_REF].

Formalizing metatheoretical results about logic, proof systems, and reasoning tools is an attractive proposition for many researchers in our field. Landmark achievements in the 1980s and 1990s include Shankar's proof of Gödel's first incompleteness theorem in Nqthm [START_REF] Shankar | Metamathematics, Machines, and Gödel's Proof[END_REF], Persson's completeness proof for intuitionistic predicate logic in ALF [START_REF] Persson | Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory[END_REF], and Harrison's formalization of basic first-order model theory in HOL Light [START_REF] Harrison | Formalizing Basic First Order Model Theory[END_REF]. Following Shankar's 1984 proof, Gödel's first incompleteness theorem has been formalized in Coq by O'Connor [START_REF] Russell | Essential Incompleteness of Arithmetic Verified by Coq[END_REF], in HOL Light by Harrison (in unpublished work), and in Isabelle/HOL by Paulson [START_REF] Paulson | Gödel's Incompleteness Theorems[END_REF][START_REF] Paulson | A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle[END_REF]. Paulson also succeeded at verifying the second incompleteness theorem.

The completeness theorem for first-order logic has been mechanized many times in proof assistants. In Isabelle/HOL, Berghofer [START_REF] Berghofer | First-Order Logic According to Fitting[END_REF] proved the completeness of a natural deduction calculus, and Margetson and Ridge [START_REF] Ridge | A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic[END_REF][START_REF] Ridge | A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic[END_REF] proved soundness, completeness, and cut-elimination of a sequent calculus for a term-free first-order logic. I refer to a recent article I wrote with Popescu and Traytel [START_REF] Christian Blanchette | Soundness and Completeness Proofs by Coinductive Methods[END_REF] for a discussion of such work.

Term rewriting is another popular target of formalization. The CoLoR library by Blanqui and Koprowski [START_REF] Blanqui | CoLoR: A Coq Library on Well-founded Rewrite Relations and Its Application to the Automated Verification of Termination Certificates[END_REF] and the CiME3 toolkit by Contejean et al. [START_REF] Contejean | Automated Certified Proofs with CiME3[END_REF], both in Coq, as well as IsaFoR [START_REF] Thiemann | Certification of Termination Proofs using CeTA[END_REF] in Isabelle, have explored this territory. They include not only formalized metatheory but also verified (non)termination and (non)confluence checkers built on it.

SAT solving also lends itself particularly well to formalization. Marić [START_REF] Marić | Formal Verification of Modern SAT Solvers[END_REF][START_REF] Marić | Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL[END_REF] verified a CDCL-based SAT solver in Isabelle/HOL, including watched literals, as a purely functional program. He also formalized the abstract CDCL calculus by Nieuwenhuis et al. and, together with Janičić [START_REF] Marić | Formalization of Abstract State Transition Systems for SAT[END_REF], the more implementation-oriented calculus by Krstić and Goel [START_REF] Krstić | Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL[END_REF]. As a milestone towards verified SMT solvers, Spasić and Marić [START_REF] Spasić | Formalization of Incremental Simplex Algorithm by Stepwise Refinement[END_REF] formalized the simplex algorithm in Isabelle. Thiemann extended this work to support incremental solving and provide unsatisfiable cores [START_REF] Marić | An Incremental Simplex Algorithm with Unsatisfiable Core Generation[END_REF]. In Coq, Lescuyer [START_REF] Lescuyer | Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq[END_REF] formalized the CDCL calculus and the core of an SMT solver. Another verification of a CDCL-based SAT solver, including termination but excluding two watched literals, is by Shankar and Vaucher [START_REF] Shankar | The Mechanical Verification of a DPLL-Based Satisfiability Solver[END_REF] in PVS. Most of this work was carried out by Vaucher during a brief internship. Finally, Oe et al. [START_REF] Oe | versat: A Verified Modern SAT Solver[END_REF] used Guru to specify and verify versat. The generated C program consists of 15 000 lines of code. Optimized data structures are implemented, including the two-watchedliteral scheme. However, termination is not guaranteed, and model soundness is established through a run-time check.

A pragmatic approach to obtain trustworthy unsatisfiability judgments from a SAT solver is to have it produce a certificate, which can be given to an independent checker. An efficient format for this is DRAT [START_REF] Heule | Bridging the Gap between Easy Generation and Efficient Verification of Unsatisfiability Proofs[END_REF]. The standard DRAT checker [START_REF] Wetzler | DRAT-trim: Efficient Checking and Trimming using Expressive Clausal Proofs[END_REF] is an unverified C program, but verified checkers have now been developed by Cruz-Filipe et al. [START_REF] Cruz-Filipe | Efficient Certified RAT Verification[END_REF] and Lammich [START_REF] Lammich | Efficient Verified (UN)SAT Certificate Checking[END_REF] using ACL2, Coq, and Isabelle/HOL. I alluded, in the introduction, to the self-referential thrill of formalizing theorem provers. Barras [5] took this idea to its logical extreme with his "Coq in Coq" Ph.D. project: a verification in Coq of a type checker for the calculus of inductive constructions underlying Coq. Analogously, Harrison [START_REF] Harrison | Towards Self-Verification of HOL Light[END_REF] verified HOL Light's inference kernel in HOL Light. To circumvent the impossibility of defining higherorder logic's semantics in itself, he carried out two distinct proofs: one where the formalized logic has no infinity axiom, and one where HOL Light is extended with an axiom to increase its strength. This formalization was ported to HOL4 and extended by Kumar et al. [START_REF] Kumar | Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation[END_REF] to include definitional mechanisms and to exploit CakeML [START_REF] Kumar | CakeML: A Verified Implementation of ML[END_REF], a verified ML environment. In another line of work, Davis built an ACL2-style prover called Milawa [START_REF] Davis | A Self-Verifying Theorem Prover[END_REF]. The development consists of a stack of provers, each used to verify the one above it. Together with Davis, Myreen [START_REF] Myreen | The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It)[END_REF] connected Milawa to a verified Lisp implementation [START_REF] Myreen | A Verified Runtime for a Verified Theorem Prover[END_REF] that was developed for hosting Milawa. A noteworthy feature of the prover is its switch command, which lets the user replace the inference kernel by an arbitrary kernel that has been proved sound, enabling powerful, highly optimized extensions that would be impossible using a traditional LCF architecture [START_REF] Gordon | From LCF to HOL: A Short History[END_REF].

Conclusion

In this paper, I reported on some of the steps my colleagues and I have taken to help drive the adoption of proof assistants in the automated reasoning community. Far from following a definite plan, at every turn we focused on topics that appealed to us and for which we could perceive clear value in formalization. We have barely scratched the surface; a lot of exciting work still awaits us.

Automated reasoning is near ideal territory for proof assistants. Compared with other application areas, the proof obligations are manageable, and little background theory needs to be formalized before we can get started. Conveniently, researchers in the area are not afraid of logic, although they often lack familiarity with proof assistants and their higher-order formalisms.

Isabelle/HOL has been a very suitable vehicle for this kind of work, and we will continue using it. It is comparatively easy to use, has a simple but expressive logic, is based on a trustworthy LCF-style inference kernel, and includes rich libraries developed by a large, and growing, user base.

  minutes per problem. The table below shows the number of solved problems, whether satisfiable or unsatisfiable, for each system:

	Glucose CaDiCaL MiniSat IsaSAT versat
	1670	1645	1361	731	357

https://bitbucket.org/isafol/isafol

Font aficionados will notice the divergent preferences concerning serifs and kernings. Pronunciation is also crucial: to avoid confusion, Japanophiles should clearly articulate izaforu (IsaFoL) and izafō (IsaFoR).

A CDCL SAT SolverAs part of a 2015 M.Sc. internship in Saarbrücken, Fleury started formalizing Weidenbach's textbook draft, tentatively called Automated Reasoning-the Art of Generic Problem Solving. He continued as a Ph.D. student, focusing largely on SAT solving and the conflict-driven clause learning (CDCL) calculus implemented in most modern SAT solvers.

http://matryoshka.gforge.inria.fr/

Acknowledgments I am grateful to all contributors to the IsaFoL effort, listed in the introduction, and to our colleagues Maximilian Kirchmeier, Christian Sternagel, Uwe Waldmann, Daniel Wand, and Christoph Weidenbach. This paper would not have existed without the dedicated labor of Heiko Becker, Alexander Bentkamp, Mathias Fleury, Peter Lammich, Anders Schlichtkrull, and Dmitriy Traytel; and the research program might never have started without the early support and advice of Tobias Nipkow, Andrei Popescu, Dmitriy Traytel, Jørgen Villadsen, and Christoph Weidenbach. Discussions with Franz Baader, Carsten Fuhs, Marijn Heule, Cynthia Kop, Leonardo de Moura, Michael Norrish, Lawrence Paulson, Giles Reger, Stephan Schulz, Natarajan Shankar, Cesare Tinelli, Andrei Voronkov, and many others have influenced this research. The Isabelle development team and the editors of the Archive of Formal Proofs have made the work possible.

I thank Assia Mahboubi and Magnus Myreen for the invitation to write in these pages and for their useful comments. Alexander Bentkamp, Mathias Fleury, Pascal Fontaine, Robert Lewis, Anders Schlichtkrull, Mark Summerfield, Christian Sternagel, Sophie Tourret, and Dmitriy Traytel suggested many textual improvements. I should also acknowledge that parts of the text have appeared in a similar form in my earlier papers [13,22,33,88,89].

The research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). My work was also partially supported by a Deutsche Forschungsgemeinschaft (DFG) project (grant Ni 491/14-1, Hardening the Hammer).