Sameh Baccari
email: sameh_baccari@yahoo.fr

Florence Mendes+
email: florence.mendes@checksem.fr

Christophe Nicolle+
email: cnicolle@u-bourgogne.fr

Fayrouz Soualah-Alila+
email: fayrouz.soualah-alila@checksem.fr

Mahmoud Neji
email: mahmoud.neji@fsegs.rnu.tn

Comparative study of the mobile learning architectures

Keywords: Mobile Technology, M-learning, Context, Adaptation, Learning method

With the emergence of mobile devices (Smart Phone, PDA, UMPC, game consoles, etc.), learning is changing from electronic learning (e-Learning) to mobile learning (m-learning). In fact, due to the mobility feature, it seems that the m-learning have to be adapted with the change within the context. Several researches addressed this issue and implemented a mobile learning environment to prove its usefulness and feasibility in various domains. In this article, we conduct a comparative study between a list of mobile learning architectures and methods that are presented in the literature. The performance of these architectures is evaluated based on several criteria, such as the adaptation management, which is an important parameter for the management and customization of the learning resources for the learners, as well as the environment, which is a core part of mobile learning systems.

Introduction

Mobile learning has become an important issue for educators and computer scientists. Thanks to large number of practical suggestions, the learner can continue his education using a mobile device whether a Smartphone or a tablet. M-learning objects can take many forms such as text, audio or video documents organized into comprehensive training programs adapted to mobile devices. While, there are a large number of courses available on mobile devices, this type of training is still at an early stage. The adaptation of the mobile devices with the available contents in e-Learning is sometimes difficult. In fact, the problems to migrate e-learning training course to mobile learning systems are not only limited to technical issue such as: the limitation of screen size and the band with. The management of change within the context and its impact on the training course remains a problem. In addition, even if, some contents, such as audio and video media course materials, are ideally suitable for mobile use, the existing systems are still unsatisfactory for the users' needs. Our goal is to check existing mobile-learning methods in order to identify how they resolve the technical heterogeneity and bridge the gap change management during the mobile learning process.

The remainder of this article is organized as follows. In Section 2, we give a brief definition of the mobile learning. Then, the context and the opportunities of contextaware applications are described in more detail in Section 3. Then, in Section 4, a list of some existing works in the literature is presented. Then a comparison between the different architectures presented in these works is established using a list of significant criteria. Finally, in Section 6, a conclusion is drawn.

Mobile learning

M-learning is described by the use of mobile and wireless technologies allowing anyone to access information and learning materials regardless of the place and at any time. Some approaches consider that mobile learning is simply an extension of the Elearning. However, these approaches do not take into account the limitations of the mobile device and the particular circumstances of mobile learning and the added value of mobility such as learning on demand, in context, through contexts, informal, etc. Mobile learning has been defined as: the process of learning and teaching that occurs with the use of mobile devices providing flexible on-demand access (without time and device constraints) to educational resources, experts, peers and services from any place [START_REF] Sharples | Guest editorial: special issue on mobile and ubiquitous technologies for learning[END_REF].

This evolution of learning can be characterized by the following changes: the introduction of distance in e-learning, and the taking account of mobility with mlearning and omnipresence with the ubiquity ubiquitous learning (ubiquitous learning, pervasive learning). These steps reflect the impact of computer technology, such as mobile and ubiquitous computing.

The shift from e-learning to mobile learning has given rise to much debate among researchers. An example, Sharma noticed that the shift from e-learning to mobile learning is accompanied by a change in the terminology [START_REF] Sharma | Web Services Architecture for M-Learning[END_REF]: shown in Table 1. The main benefits of mobile learning for education and learning are reported as follows [START_REF] Lam | A review of mobile learning in the mobile age[END_REF]: (a) enables on-demand access to learning resources and services, as well as instant delivery of notifications and reminders, (b) offers new opportunities for learning that extend beyond the traditional teacher-led classroom-based activities, (c) encourage learners to participate more actively in the learning process by engaging them to authentic and situated learning embedded in real-life context and (d) supports on-demand access, communication and exchange of knowledge with experts, peers and communities of practice.

One big difference between learning somewhere on a stationary desktop computer and learning with mobile devices is the context, the user is in. Mobile devices feature some functionality to capture some background information that can be helpful to personalize the learning experience. When considering mobility from the learner's point of view, rather than the technology's, it is more important to say that m-learning is about people moving through environments, learning as they go, using electronic devices that enables connectivity to information sources and communication while they are able to change their physical location. In short, our new definition of mobile learning is "context-aware learning". The context-aware concept is discussed in some detail in the next sections.

Mobile learning in context

In a mobile learning experience, each learner has to be treated in a different way according to the current situation in which he is learning, e.g. according to his preknowledge or the specifications of the device, he is using. Those different conditions are called the context in which the learner is situated.

The term "context-aware" was brought and defined by Schilit et al. [START_REF] Schilit | Context-aware computing applications[END_REF] to describe the location, identities of nearby people, objects and changes to the objects. Currently such terminology is used in various research disciplines; linguists provide two meanings for it. Context can be defined as the text in which a word or a passage appears and which helps to ascertain its meaning.

A very popular definition is given by Dey [START_REF] Dey | Understanding and using context[END_REF] who define context as "… any information that can be used to characterize the situation of an entity. An entity is a person, place, or object that is considered relevant to the interaction between the user and the application, including the user and the applications themselves." In mlearning, the context has been proposed to be modelled into two parts: one related to the learning design and another related to the mobile environment in which learners interact by completing learning activities [START_REF] Pachler | Mobile learning: Structures, agency, practices[END_REF]. These two categories are referred to as learning context and mobile context [START_REF] Siadaty | m-LOCO: An Ontology-based Framework for Context-Aware Mobile Learning[END_REF].

Learning context can be described by the elements of a learning design. A learning design is defined as:

" the description of the teaching-learning process, which follows a specific pedagogical modelor practice that takes place in a unit of learning (e.g., a course, a learning activity or any other designed learning event) towards addressing specific learning objectives, for a specific target group in a specific context or subject domain" [START_REF] Koper | Representing the Learning Design of Units of Learning[END_REF].

Mobile context can be referred to as contextual information such as people, technological artifacts, learner's location and its physical conditions, available time, etc., which can be captured by hardware, measured by sensors or even entered by the learner. We are considering a classification of the mobile context characteristics with eight dimensions based on characteristics defined by mobile context-related research works [START_REF] Kukulska-Hulme | Practitioners as Innovators: Emergent Practice in Personal Mobile Teaching, Learning, Work, and Leisure[END_REF].

Harnessing context in a mobile learning experience has a wide range of benefits including personalization, adaptation, intelligent feedback, and recommendation.

Adding context information to an application may lead to presenting more personalized data to the learner. If there is no context information available, every learner has to be treated the same way. Context may contain information about the current situation, in which the learner is in, her pace, knowledge, interest, peers, motivation, etc. This knowledge enables applications to present only those parts of the learning activity that are of interest in that special situation [START_REF] Thüs | Towards a dynamic process model of context[END_REF]. Context-aware mobile learning systems can adapt to every situation, give intelligent feedback to the preceding learning process, and produce recommendations for new learning items or activities.

Subsequently, the focus will be on the studies which implemented a mobile learning environment to prove their usefulness and feasibility in different domains.

Previous works

In this section, we will review the work existing in the literature by presenting representative approaches and platforms of mobile learning. The interest is in the adaptation management, which is a very important parameter in managing and customizing the learning resources to the learners. The focus will also be on the context, which is a central core of all the mobile learning systems.

MOBILearn is a European research and development project which aims at exploring the use of mobile environments to foster informal learning, learning through problem solving and learning at work. As part of this project, a new architecture for mobile learning was constructed. It can help generate contents and services to accompany a learner during his learning activities in a gallery or a museum [12]. Learning is backed by a set of activities at the museums. Being placed in front of a painting, the visitors can then use a PDA or Smartphone to get the relevant information while observing the painting in order to learn. A learner visiting a museum for the second time can acquire information related to his previous visit.

eBag is part of the iSchool project for nomadic and mobile learning [START_REF] Brodersen | eBag: a ubiquitous Web infrastructure for nomadic learning[END_REF] for which mobility and context are two key elements. In short, the iSchool project vision is to develop a software infrastructure, graphical interfaces and spatial concepts in an interactive environment. The idea behind eBag is the creation of a "virtual schoolbag" for each student to help him learn through contexts by moving to specific locations (classrooms, laboratories, workshops, libraries, museums, cities, clubs and at home). The objective of the system is therefore to serve as a "personal and digital warehouse" in which all the resources (texts, photos, videos, etc.) can be stored for internal and external use of the school environment.

The MoULe project (Mobile and Ubiquitous Learning) aims to suggest that the pupils use mobile devices to build up collaborative knowledge. It also aims at the use of mobile devices incorporating learning activities in the classroom and laboratory for situation learning. The MoULe is an environment that helps the users edit and share documents and concept maps using desktop computers and smart phones equipped with GPS. The latter ones enable students to collect textual content, images, videos and audio recordings while visiting an outside site during their learning activities. The system also helps them comment on the media they collect to classify it so that their research and the re-use of the information in collaborative activities will be easy [START_REF] Arrigo | A Collaborative M-Learning Environment[END_REF].

The CoMoLE project is a platform called adaptive based on Context-Mobile Learning Environments. The users can access the environments supported by CoMoLE different devices via a Web browser. CoMoLE supports the recommendation and the fulfillment of various types of learning activities, such as reading comprehensions, observing examples, doing tests and short unanswered exercises, solving problems together, downloading e-materials for their study, sending/receiving messages to/from partners of the same workgroup, and so on. The activities may have associated multimedia content and collaboration tools to support the interaction between the members of the same group in the case of collaborative activities. Each activity can be devoted to everyone, to certain types of users, or only to users in specific contexts. These coping capacities are defined by rules [START_REF] Martin | Supporting the development of mobile adaptive learning environments: a case study[END_REF].

Nguyen Pham and Ho present CAMLES (Context-Aware m-Learning System) to help students learn English as a foreign language to prepare them for TOEFL test by suggesting topics that they need to learn on the basis of their test results. The test provides an adaptive content for different learners in context, including location, time and the learner's knowledge [START_REF] Nguyen | A Context -Aware Mobile Learning Adaptive System for Supporting Foreigner Learning English[END_REF].

Chuantao YIN proposed the design for a contextual mobile learning system known as SAMCCO (French abbreviation for "contextual and collaborative mobile learning system for professional fields") [START_REF] Yin | SAMCCO : a System of Contextual and Collaborative Mobile Learning in the Professional Situations[END_REF]. This system is based on EPSS (Electronic Performance Support System), the goal of which is to group storage of technical, working and learning data in order to provide just-in-time, just enough training, information, tools and help for mastering or repairing equipment, appliances or products disseminated in the smart city environment. This system is able to provide appropriate information designed to maintain or ensure appropriate performance of smart city users when and where needed, thereby also enhancing the performance of the company as a whole and industry. EPSS is used to store and deliver plant reference materials including: training documents, operating procedures and historical maintenance information. SAMCCO edits and organizes learning contents stored in the EPSS information database, which is an essential professional learning resource offering abundant and well-structured learning contents.

In 2013, Soualah et al [START_REF] Soualah Alila | A Context-Based Adaptation In Mobile Learning[END_REF] proposed approach for context-based adaptation for m-earning, making use of learning practices already deployed in e-learning systems and adopting them in m-learning. This system is built around an ontology that both defines the learning domain and supports context-awareness. The use of this ontology facilitates context acquisition and enables a standard-based learning object metadata annotation. They also use a set of ontological rules to achieve personalized contextaware LOs by exploiting knowledge embedded in the ontology. The future adaptive system will offer an optimized panel of LOs matching with the current context of the learner.

The UoLmP project (Units of Learning Mobile Player) Project [20] is intended to present an adaptive and personalized mobile learning system, context sensitive, which aims to support the semi-automatic adaptation of the learning activities. This is about: (a) the accommodations to the interconnection of the learning activities (i.e. the learning flow) and (b) to the educational resources, tools and services that support the learning activities. The initial results of the assessment of the UoLmP use provide evidence that UoLmP can successfully be adapted to the learning flow of a pedagogical scenario and the provision of educational resources, tools and services that support the learning activities. Finally, these accommodations can help students successfully complete the learning activities of a pedagogical scenario. Some of them will then be analyzed in the mobile learning systems that have been performed to show the features of the mobile learning mentioned in the previous section.

Analyses and Discussion

In this section we give a comparative study of the different approaches and architectures of mobile learning that we have presented in the previous section. This comparison is based on some significant criteria and features, we are particularly interested in device mobile support, heterogeneity support, reduce the bandwidth use, adaptability, traceability and control, learning is seen as activities in context, learning context-Aware, learning as a collaborative process, the integration of formal and informal learning, mobile learning -part of a whole. The result of this comparison is presented in table 2.The analysis of the existing studies has given us an overview of the opportunities provided by the mobile learning environments based on the individual needs. In fact, most of these studies enable learning in different locations (in the classroom, outdoors, in a museum, in companies, etc.).

Table 2.Comparative Study architectures of mobile learning

The most important feature that characterizes the works presented in soualah et al, SAMCCO and UoLmP projects is the Mobile learning in context. In fact, UoLmP can successfully be adapted to the learning flow of a lesson plan and to the provision of educational resources, tools and services that support the learning activities. SAMCCO is based on AM-LOM metadata and ontology, which are used in the learning unit model to describe and identify contextual mobile learning contents particularly in the professional field. Among the projects that are interested in the collaborative learning, we find CAMLES project. This project has considered the role of participants and the pedagogical purposes (collaborative missions) and supports. However, the MoULe project has helped teachers to organize scenarios in a limited way. We have remarked that most approaches do not enable the adaptation between the course content and the learner's profiles. Context-aware approaches have the advantage of providing the user the appropriate learning resources depending on the context. It is therefore essential to determine, depending on the context, how, when, and on which interface the resources should be sent. However, Learning Through contextualization is not easy to achieve. In fact, the development of mobile technologies and the dynamics in the mobile environments have complicated the process of contextualization. Today, mobile computing (user mobility, terminal mobility, and network mobility) is characterized by a permanent change in context (connected or disconnected, low or high bandwidth, change of location, widescreen or small screen, varying input devices, etc). Thus, it has become very complex, to consider many and various aspects when designing such application. Mobile learning is very important particularly in education, and the major utilization of mobile devices is in the field of medicine. In fact, medical students are placed in hospital/clinical require in their training an access to course information while on the move. In addition, the work of the postgraduates and the physicians involves a high degree of mobility between distributed sites and instant communications within work environments. Distributed sites where physicians are working and in which students are placed are often in remote and rural areas. The technological advances can be capitalized to promote and facilitate situated learning. In fact, face the considerable growth of data, the heterogeneity of roles and needs and the rapid development of mobile systems, it becomes important to provide a system able to provide the user with a pertinent training adapted to their needs. This system requires a context-aware architecture, with mechanisms the change within the context. This architecture must take into account the different characteristics of the user as well as all of the contextual situations that influence their behavior when interacting with the mobile learning system.

Conclusions

In this article, we presented and compared the list of architectures of mobile learning according to a list of features. All the presented architectures are not able to detect the mobile learning environment or to get information about it. Therefore, they cannot be adapted. Our work is an extension of one of the presented m-learning approaches in which we propose the context management, the adaptation and the learning without a break through contexts. Our goal is to design a mobile learning architecture that supports the features of mobility and context in order to enhance the learning experience in the field of education, specifically in medical field.

Table 1 .

 1 Comparison of e-learning terminology and mobile learning (according to[START_REF] Laouris | We Need an Educationally Relevant Definition of Mobile Learning[END_REF])

	E-learning	M-learning
	Computer	Mobile
	Bandwidth	GPRS, 3G, Bluetooth
	Multimedia	Objects
	Interactive	Spontaneous
	Hyperlinked	Connected
	Distance learning	Situated learning
	More formal	Informal
	Simulated situation	Realistic situation
	Hyper learning	Constructivism, situationism, collaborative
	In classroom or internet labs	In the field or while mobile


Roberto Blanco
email: roberto.blanco@inria.fr

Tomer Libal
email: tomer.libal@inria.fr

Dale Miller
email: dale.miller@inria.fr

Defining the meaning of TPTP formatted proofs

The TPTP library is one of the leading problem libraries in the automated theorem proving community. Over time, support was added for problems beyond those in first-order clausal form. TPTP has also been augmented with support for various proof formats output by theorem provers. Such proofs can also be maintained in the TSTP proof library. In this paper we propose an extension of this framework to support the semantic specification of the inference rules used in proofs.

Introduction

A key element in optimizing the performance of systems is the ability to compare them on common benchmarks. In the automated theorem proving community, such benchmarks are available via the "Thousands of Problems for Theorem Provers" (TPTP) library [START_REF] Sutcliffe | The tptp problem library and associated infrastructure[END_REF]. A part of the library's success lies in its syntactic conventions, which are both intuitive to read and rich enough to encode many kinds of problems. Another advantage of its syntax is its simple structure that allows one to easily write parsers and other utilities for it. As part of the evolution of the library and its syntax, a support for proofs was added. In order to support the proof library, called "Thousands of Solutions from Theorem Provers" (TSTP), the syntax needed to be extended to support different types of proofs, in particular, directed acyclic graph proofs. This syntax allows for the description of proofs as a series of steps which are themselves encoded collections of inference rules and some additional annotations. One shortcoming of this format is its emphasis on syntax and its inability to describe precisely the semantics of the inferences used.

The increased complexity of today's automated theorem provers has brought with it a need for proof certification. Errors in proofs can result from several sources ranging from bugs in the code to inconsistencies in the object theory. In order to improve this situation, several tools for proof certification have been implemented that can improve our confidence in the proofs output from theorem provers. These tools can be classified into two groups. First it is possible to actually prove that a theorem prover is formally correct (see, for example, Ridge and Margetson [START_REF] Ridge | A mechanically verified, sound and complete theorem prover for first order logic[END_REF]). The second group consists of tools for verifying, not the theorem provers themselves, but their output. This group can be further divided into two groups. The first group consist of systems for replaying proofs using external theorem provers for verifying specific steps. Among these, one can count the general tools Sledgehammer [START_REF] Lawrence | Source-level proof reconstruction for interactive theorem proving[END_REF][START_REF] Böhme | Sledgehammer: judgement day[END_REF], PRocH [START_REF] Kaliszyk | Proch: Proof reconstruction for hol light[END_REF] and GDV [START_REF] Sutcliffe | Semantic derivation verification: Techniques and implementation[END_REF] as well as more specific efforts such as the verification of E prover [START_REF] Schulz | System description: E 1.8[END_REF] proofs using Metis [START_REF] Lawrence | Source-level proof reconstruction for interactive theorem proving[END_REF]. The second group contains tools having an encoding or a translation of the semantics of theorem provers, which is then used in the replaying process. This last group can be divided again into specific tools, such as Ivy [START_REF] Mccune | Ivy: A preprocessor and proof checker for first-order logic[END_REF] and the encodings of MESON [START_REF] Loveland | Mechanical theorem-proving by model elimination[END_REF] and Metis [START_REF] Hurd | First-order proof tactics in higher-order logic theorem provers[END_REF] in HOL Light and Isabelle, respectively, and general tools such as Dedukti [START_REF] Boespflug | The λΠ-calculus modulo as a universal proof language[END_REF] and ProofCert [START_REF] Miller | A proposal for broad spectrum proof certificates[END_REF].

These various classes of tools represent different approaches to proof certification. While we can have a high level of trust in the correctness of the provers in the first group, their performance cannot be compared to that of the leading theorem provers like E [START_REF] Schulz | System description: E 1.8[END_REF] and Vampire [START_REF] Riazanov | The design and implementation of VAMPIRE[END_REF]. The remaining groups do not pose restrictions on the provers themselves but the generality and automation of those in the second group come with the cost of using an external theorem prover and translations, which might result in reduced confidence. The last two groups require an understanding of a theorem prover's semantics so that one can guarantee the soundness of proofs by their reconstruction in a low level formal logic. Working with an actual proof has several advantages as one can apply proof transformations and other procedures. The last group has additional advantages over the previous one: a single certifier can be written that should be able to check proofs from a range of different systems and the existence of a common language for proofs allows for the creation of proof libraries and marketplaces [START_REF] Miller | A proposal for broad spectrum proof certificates[END_REF].

Those tools in the last group have, so far, only limited success in the general community. One reason for this is that understanding and specifying the semantics of proofs requires sophistication in the interplay between deduction and computation (whether via function-style rewriting or proof-search).

The difficulty in understanding the semantics of the object calculi lies in the gap between the implementers of theorem provers and the implementers of the proof certifiers. Currently, the normal process for certifying the output of a certain theorem prover is for a dedicated team on the certifier side to try to understand the semantics of each inference rule of the object calculus. This approach suffers many times from missing documentation, different names and versions of actual software, and insufficient information in the proofs themselves [START_REF] Chihani | The proof certifier checkers[END_REF]. This gap is enlarged by the fact that teams of implementers and certifiers can reside in different locations or even work in different periods, thus making the communication between them difficult or even impossible.

One way to overcome this gap is to supply the implementers of theorem provers with an easy to use and well-known format in which to describe the semantics of their inference rules. This format should be general enough to allow specifications to range from precise (functional) definitions-translating a proof in the object calculus into a proof in another, trusted and wellknown calculus-and informal definitions, with hints on the right way to understand the object calculus without needing to specify how to actually reconstruct a formal proof.

In this paper we aim at helping to reduce the gap mentioned above between those who produce proofs and those who must certify them. We propose to use a format which is wellknown to the implementers of theorem provers-the TPTP format itself-for the purpose of describing not only problems and proofs but also the semantics of proofs. This will make a TPTP file an independent unit of information which can be used for certification as well.

An additional advantage of using the TPTP format to specify semantics is the same one mentioned above for building tools for the TPTP library. The predicate logic form of the problems, their solutions, and now, also their semantics, will allow proof certifiers to easily access the semantics and will further diminish the gap between the theorem provers and their certifiers. For example, the checkers proof certifier [START_REF] Chihani | The proof certifier checkers[END_REF] (written using logic programming), will only require minor computations to be applied to the input files, if any. Such simplicity helps to improve the trust of the certification process.

The paper is organized as follows. In the next section we present and describe both the TPTP syntax and the notion of using predicates in order to define the semantics of logics. In section 3 we present and discuss the minor augmentations needed in the TPTP format in order to support the ability to use this format to denote semantics. Section 4 is devoted to the full description of four examples from four different theorem provers. The concluding section suggests some additional advantages of using this approach.

Preliminaries

Syntax in TPTP

A beneficial side effect of the TPTP library as a standard test suite for automated theorem provers is the standardization of a language to express logic problems and their solutions. It is no coincidence that this standardization on the language is credited as one of the keys to the success of the TPTP project [START_REF] Sutcliffe | The tptp problem library and associated infrastructure[END_REF].

The TPTP syntax is built upon a core language called THF0 [START_REF] Benzmüller | THF0-the core of the TPTP language for higher-order logic[END_REF]. This core can be restricted to support a number of interface languages: untyped first-order logic as first-order form (fof) and clause normal form (cnf), typed first-order form (tff), and typed higher-order (thf). Furthermore, all of these can be used in combination with a process instruction language (tpi) for the manipulation of formulas. The concrete syntax revolves around the concept of annotated formulas and is expressive enough to structure proofs and embed arbitrarily complex information as annotations.

Among the stated design goals of the format, both extensibility and readability (by machines and logicians) figure prominently. In addition, care has been taken to ensure that the grammar remains compatible with the logic programming paradigm, and TPTP documents are, in fact, valid Prolog programs.

For defining a formula using the TPTP format, one uses the following templates:

Language ( Name , Role , Formula ). Language ( Name , Role , Formula , Annotations ).

where Language ∈ {cnf,fof,tff,thf,tpi} (see above for the list of interface languages), Role describes the role of the formula -i.e. 'axiom' or 'type'-, Formula is the encoding of the formula in the specified language and Annotations contains optional additional information.

A template for defining structural derivations is the following:

Language ( Name , Role , Formula , inference ( Rule , Info , Parents )).

Here Rule denotes the name of the inference rules used, Info optionally specifies additional information, like the SZS output value of the inference and Parents also optionally refers to the names of the formulas which were used in the application of this rule. Formula, as before, is an encoding of the derived formula in the respective language. The SZS ontology [START_REF] Sutcliffe | The szs ontologies for automated reasoning software[END_REF] referred to above supplies a set of inference properties, such as theoremhood, satisfiability, etc., which give some semantical information. It should be noted that this information might suffice for proof replaying using an external prover [START_REF] Lawrence | Source-level proof reconstruction for interactive theorem proving[END_REF][START_REF] Kaliszyk | Proch: Proof reconstruction for hol light[END_REF][START_REF] Sutcliffe | Semantic derivation verification: Techniques and implementation[END_REF], but does not fully help in understanding the semantics of the inference rules themselves. Another useful feature of TPTP is the include directive, which performs a syntactical inclusion of one file into another. This directive may help reduce redundancies.

Denoting semantics as logic programs

As already mentioned, one way to formally describe the semantics of an inference rule is by translating an instance of this rule into a derivation in another, well-known, calculus. This translation can be determinate or nondeterminate: in the latter case, a logic programming implementation of the translation could allow for that nondeterminism to be explored using backtracking search. Nondeterminism in the specification of proof semantics has been considered in other systems as well. In particular, nondeterminism is allowed in the Foundational Proof Certificates (FPC) framework [START_REF] Chihani | Foundational proof certificates in first-order logic[END_REF][START_REF] Miller | A proposal for broad spectrum proof certificates[END_REF] where client-side inference rules (i.e., rules implemented in theorem provers) are translated into low-level rules of sequent calculus. The checkers proof certifier [START_REF] Chihani | The proof certifier checkers[END_REF], based on the FPC framework, used the λProlog logic programming language [START_REF] Miller | Programming with Higher-Order Logic[END_REF] to provide for a backtracking search approach to exploring any nondeterminism in such translations. The basic idea is to program a set of predicates which will guide the search in the target calculus. By guiding the search for a derivation of an instance of an inference rule in a well-known calculus, this set of predicates can be considered as denoting the semantics of this inference.

Before describing how we plan to use the TPTP framework to specify the translation of inference rules, we need to present the underlying principles behind the idea.

First, and critically, semantic descriptions are not "one size fits all": there is an underlying trade-off between space (for storing a proof) and time (for checking a proof). More detailed semantic translations, insofar as the information provided is useful, produce more efficient verifications; conversely, high-level, conceptual descriptions may serve as guidance but cannot be used to generate a constructive decision procedure without additional information or search. At one extreme are fully determinate translations of inference rules and at the other extreme are minimal but sufficient hints to allow a possible reconstruction of a proof in an independent checker. In contrast, here we consider the full spectrum of implicit vs. explicit reconstruction.

For example, suppose we wish to obtain a proof of a formula A ∧ B ∧ C. It may simply be stated that to do this, separate proofs for A, B, and C are needed:

A B C A ∧ B ∧ C
To understand the meaning of this inference rule, one can try to infer the conclusion from the hypotheses using a well-known calculus, the sequent calculus for example, which tells us that in order to derive the original goal, two proofs are needed, one for A and a second one for B ∧ C, and then divide in turn this second composite proof into sub-proofs of B and C:

A B C B ∧ C A ∧ B ∧ C
The question of whether we can trust the first inference relies on the fact that its semantics is defined by the second, in the sense that it constitutes a formal derivation of the intended meaning, namely, that one can obtain a proof of the conjunction of three goals from proofs of each of those goals. Trust in the calculus of choice extends to trust in the inference rules that it can justify. Contrariwise, consider an alternative candidate for an inference rule:

A B C A ∨ B ∨ C
It can be proved that a reasonable calculus will be unable to derive an inference of this shape. In the absence of a trustworthy proof reconstruction of the postulated inference rule, its validity cannot be accepted.

Consider now the more realistic case of paramodulation [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF], a concrete instance of which we study in section 4.1. In this case, an explicit functional translation of the formal definition is far from being trivial. Conversely, it may be stated, more informally, that paramodulation handles equality modulo reflexivity: that is to say, the transitivity and symmetry axioms can be used to simulate this rule in a logic without explicit handling of equality (note that reflexivity axioms must be given externally for the equality procedure to be complete).

By applying some additional effort, this approach was implemented successfully in checkers and is capable of guiding the proof search for arbitrary instances of the paramodulation rule. This implies, therefore, that supplying the two axioms provides enough information to assist the automatic certification of this inference rule.

3 Thousands of Semantically Annotated Solutions for Theorem Provers (TATP)

In order to have the cleanest and most declarative treatment of one logic (i.e, the logic of the client prover) within a second logic encoding inference rules and their associated proof search, we shall make use of the notion of order of THF0. In this setting, defining the semantics of logical formulas of order n employs a meta-level logic of order n + 1. For example, if our client proofs are only propositional formulas (order 0) then the first-order fragment of THF0 suffices. However, if our client proofs are first-order formulas, then we employ directly the second-order subset of THF0. As seen in section 2, TPTP is equipped with the necessary syntax necessary to define formulas of an arbitrary finite order. It is largely for this reason that we will employ λProlog [START_REF] Miller | Programming with Higher-Order Logic[END_REF] to automate1 the translation of inference rules, since the logic underlying λProlog is close to that underlying THF0 (both are closely related to Church's Simple Theory of Types [START_REF] Church | A formulation of the Simple Theory of Types[END_REF]). For example, in order to define the provability (via the predicate pr) of a classical first-order quantifier, one can use the following λProlog clause:

pr(∀x.Bx) :-Πx. pr(Bx).
where ∀ is the object-logic universal quantifier and Π is the meta-level universal quantifier. The implementation of λProlog deals directly with the many issues related to binding, substitutions, eigenvariables, and unification [START_REF] Felty | Specifying theorem provers in a higher-order logic programming language[END_REF]. TPTP proofs are already annotated by the inference rules that are used in order to derive the formula. These annotations, however, lack a formal semantics and they cannot normally be understood by a person not familiar with the details of the system that outputs those annotations. We propose to use the TPTP thf syntax in order to allow the implementer of a theorem prover to include semantical information about their inference rules, thereby replacing imprecise and specialized annotations with more formal annotations. Note that by using the TPTP include directive, one does not need to include these definitions in every proof generated but just define them once.

In order to allow such a use, we can first define a new role for formula definitions. We therefore add the following directive to the TPTP syntax:

< formula_role > :== semantics

A TPTP semantics definition will have the following form: thf ( Name , semantics , Formula , Annotations ).

where Name, by convention, should consist of the prover name, underscore and then the inference name which was used in the proof, for example "e pm". Formula can contain an arbitrary higherorder typed formula denoting the semantics definitions. In the rest of the paper, though, we ignore typing information in order to focus on clarity. Note that the logical programming language λProlog requires formulas to be in fragment of higher-order logic called hereditary-Harrop formulas [START_REF] Miller | Programming with Higher-Order Logic[END_REF]. As has been shown elsewhere (for example, [START_REF] Felty | Specifying theorem provers in a higher-order logic programming language[END_REF] and [START_REF] Miller | Programming with Higher-Order Logic[END_REF]Chapter 9]), this fragment of logic is able to elegantly specify a variety of inference rules. Thus, if one can define the semantics of inference rules using these formulas, one could use, with minimal intervention, proof checking software like checkers to verify proofs. Lastly, Annotations can contain additional (informal) information which can help understanding the semantics. These annotations may include the name of a target logic which can be used for proof reconstruction or a reference to a paper which defines the target or object logics.

A question we still need to answer is how one can define the semantics of an inference rule and how we can make that task as simple as possible. The decision taken here is to allow the implementer of a theorem prover to use, in order to define the semantics of their own rules, the inference rules and the theory of any other calculus. In general, they can decide to specify the semantics using the inference rules of another theorem prover. However, it would be preferable to specify the semantics using the inference rules of a well known calculus, like the original resolution calculus by Robinson [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF], for example. The approach we are discussing here (with examples in the next section) stands in contrast to what is being done in the ProofCert project [START_REF] Miller | Proofcert: Broad spectrum proof certificates. An ERC Advanced Grant funded for the five years 2012-2016[END_REF]. In that project, the meanings of all inference rules are "compiled" into a low-level proof system (representing an "assembly language" for inference). We do not insist on employing that framework, opting instead for a less tedious and more high-level approach to providing some useful information about the inference rules used in a specific theorem prover.

It should be noted that according to the above conventions, one has full control over the amount of detail and choice of the target calculus. A large amount of detail might enable a precise proof reconstruction in a fine grained calculus, for example, in the sequent calculus (the ProofCert project does exactl1y this, for example). We want to stress here that since the aim of these definitions is to communicate information about the semantics, such detailed information is not necessary. There can be benefits for both the certification team and the implementers in specifying information about the semantics of their own rules using the highest level calculus known to the community. This will make the definition simpler and will also contribute to the modularity of a certification tool since the certifiers will only need to implement the semantics of the high level calculus, the semantics of which being widely known. For example, all superposition provers are using variants of the paramodulation inference rule [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF]. Defining the semantics of these variants can be done by a number of individualized, detailed descriptions or be based on the known notion of paramodulation. It seems more intuitive and simple for implementers to choose the second option and let the certification team implement the general semantics of paramodulation. This is the approach taken in checkers and described below in the examples. A fine grained description of the semantics of paramodulation can be found, for example, in [START_REF] Chihani | Proof certificates for equality reasoning[END_REF].

When defining proofs in the TPTP format, the information of which inference rule to use is supplied using the annotation directive. We will do the same and use this directive in order to supply the information of what calculus is being used to define the semantics. To this end, we will add the following directives to the TPTP syntax: < source > ::= < calculus_info > < calculus_info > ::= calculus ( < calculus_name > < optional_info >) < calculus_name > ::= < atomic_word > Using these directives, the user can specify the name of the calculus used and supply additional information, such as the name of a paper where this calculus is defined.

The last remaining task is to be able to bind the instances of the inference rules in the proofs to their semantics definitions. We suggest the following convention: in order to specify an inference call in DAG form, i.e. the ones used in proofs, the user will employ the following predicate:

<inference rule>(f, f 1 , . . . , f n )
where f is the derived formula and the remaining formulas are the inputs used in the derivation.

Examples of this convention are given next.

Examples

We demonstrate the use of THF0-style annotations on four examples taken from inference rules used by four different theorem provers.

Paramodulation in E

The E prover [START_REF] Schulz | System description: E 1.8[END_REF] was among the first provers to output proofs using the TPTP format. A staple on the podium at the annual CASC competitions [START_REF] Sutcliffe | The state of casc[END_REF], E is used by many other firstand higher-order theorem provers. E is a superposition-based, saturating, automated theorem prover based on a purely equational paradigm. As such, it implements several variants of the paramodulation rule.

Definition 1 (Paramodulation [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF]). Given clauses A and α = β ∨ B (or β = α ∨ B) having no variables in common and such that A contains a term δ, with δ and α having a most general common instance α identical to α [s i /u i ] and to δ[t j /w j ], form A by replacing in A[t j /w j ] some single occurrence of α (resulting from an occurrence of δ) by β [s i /u i ], and infer

A ∨ B[s i /u i ].
One concrete variant, for example, is given in the pm rule of E. This rule is applied in TPTP syntax using the following form: cnf ( ClauseId , Role , Formula , inference ( pm , [ status ( thm )] ,

[ SourceId1 , SourceId2 , theory ( equality )])).

where SourceId1 and SourceId2 are the two clauses to which the paramodulation rule is applied to obtain ClauseId, corresponding to the formula given by Formula and with role Role. The semantics of this rule is similar to the semantics of the paramodulation rule (from [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF] and our definition), with the peculiarity that the tactic presents symmetry for both ClauseId1 and ClauseId2.

To produce the full definition we proceed in two steps. First we present a TPTP formula that denotes the semantics of the pm rule.

thf ( eprover_pm , semantics , Formula , calculus ( paramodulation , [ p .5 in [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF] ])).

where the semantics is documented by a suitable bibliographic reference. Second, we define Formula as the mapping between the specific variation of paramodulation defined by the E prover (namely, the pm tactic) and the canonical semantics derived from the definition:

∀ SourceId1 , SourceId2 , ClauseId : pm ( SourceId1 , SourceId2 , ClauseId ) ⇐ paramodulation ( ClauseId , SourceId1 , SourceId2 ) ∨ paramodulation ( ClauseId , SourceId2 , SourceId1 )
where, as usual, free variables are universally quantified; we have made this quantification explicit in the present formulation.

Binary resolution in Vampire

Vampire [START_REF] Riazanov | The design and implementation of VAMPIRE[END_REF] is a theorem prover that implements the superposition calculus and is the regular winner of the first-order division in the CASC competition over the last decade [START_REF] Sutcliffe | The state of casc[END_REF]. Proofs proceed by saturation and rely on redundancy elimination and a wide range of advanced techniques to maximize performance, one of its original design goals. It features a rich collection of inference rules and supports the TPTP syntax, including various extensions. Here we inspect TSTP entries produced by Vampire 4.0 to infer program semantics.

Definition 2 (Binary resolution [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF]). Given two clauses A = a 1 ∨. . .∨a m and B = b 1 ∨. . .∨b n and a pair of complementary literals, one from each clause, i.e., a i = ¬b j or ¬a i = b j , the resolution rule derives a new clause with all the literals except the complementary pair:

C = a 1 ∨ . . . ∨ a i-1 ∨ a i+1 ∨ . . . ∨ a m ∨ b 1 ∨ . . . ∨ b j-1 ∨ b j+1 ∨ . . . ∨ b n .
The binary resolution rule includes the possibility of applying a unification procedure to a pair of unifiable literals, and substituting the most general unifier in the resolvent C. Some categories of binary resolution can be defined. These are not necessarily mutually exclusive:

• Positive resolution, if one of the parent clauses is a positive clause, i.e., all its literals are positive.

• Negative resolution, if one of the parent clauses is a negative clause, i.e., all its literals are negative.

• Unit resolution, if one of the parent clauses is a unit clause, i.e., formed by exactly one literal.

Vampire outputs natively to TPTP in addition to its own internal format, closer to that of Prover9 that we treat in the next subsection. Now, we consider the TPTP output of the basic resolution rule.

fof ( ClauseId , plain , Formula , inference ( resolution , [] , [ SourceId1 , SourceId2 ])).

The translation takes this to the higher-order formula and adjusts the annotation information in the inference name to point to the name of the logic program that implements the procedure.

thf ( vampire_resolution , semantics , Formula , calculus ( hol )).

where Formula is defined to be

∀ S1 , S2 , R1 , R2 : resolution ( S1 , S2 , R1 ∨ R2 ) ⇐ ∃ L : select ( S1 , L , R1 ) ∧ select ( S2 , ¬L , R2 ) ∨ select ( S1 , ¬L , R1 ) ∧ select ( S2 , L , R2 ).
Here the standard list selection predicate is used to pick a literal from a list-like clause and yield a copy of the clause without the chosen literal. We are still free to use concatenate clauses by way of a disjunction.

A clause produced by binary resolution is specified by the two premise clauses and (considering each of these in CNF form, and in turn a CNF form as an indexed list of disjuncts) by the disjunct from each clause that is involved. We also assume a predicate specifying, and therefore declaratively implementing, binary resolution, that acts on formulas and can check whether the specified application of resolution yields the target formula.

Hyperresolution in Prover9

Prover9 [START_REF] Mccune | Prover9 and mace4[END_REF] is a theorem prover based around the techniques of resolution and paramodulation, and the successor of the Otter theorem prover. The last available version is 2009-11A, dated November 2009. While development has since ceased, the tool remains in use. Prover9 does not produce output in TPTP format, and therefore TSTP contains unparsed execution traces. However, the input and output formats of the prover are simple and well documented, and their semantics can be easily formalized. Interestingly, such a translation procedure offers the possibility of generating the native TSTP output that is missing from the problem library, together with its semantics.

In this subsection we consider hyperresolution [START_REF] Christian G Fermüller | Resolution decision procedures[END_REF], one of the primary tactics used by Prover9. An informal definition of the inference rule follows.

Definition 3 (Hyperresolution [START_REF] Christian G Fermüller | Resolution decision procedures[END_REF]). Assume a nucleus clause A, nonpositive, with a number k of negative literals ¬a i1 , . . . , ¬a i k , and as many satellite clauses B 1 , . . . , B k , each of which resolves on of those negative literals, i.e., B j = . . . ∨ a ij ∨ . . .. The hyperresolution rule resolves all the negative literals in the nucleus, each with its satellite, producing a positive clause C.

Hyperresolution can be seen as a sequence of applications of binary resolution. It is likewise possible to reverse polarities and speak of negative hyperresolution. A related concept is that of unit-resulting resolution, where the satellites are unit clauses and the nucleus is reduced down to a single literal, i.e., another unit clause.

Prover9 implements this as the hyper tactic. The output language divides files in several sections, one of which contains proofs presented as justifications: a sequence of clauses, each derived from the starting clauses or by previous derivations in the chain. Inferences in each step of the justification are themselves lists of tactics: exactly one primary tactic, possibly followed by a number of secondary tactics. Hyperresolution is one of the primary tactics, and for simplicity we will consider its treatment in isolation. It will become clear that sequences of secondary steps follow an analogous compositional pattern.

An example of hyperresolution step is hyper(59, b, 47, a, c, 38, a) where clauses are referenced by Arabic numerals and literals within a clause by letters: a, b, c. . . Though represented by a plain list, it is to be interpreted as the nucleus clause followed by a sequence of triples, each specifying a satellite clause and the literals that are involved to produce the next clause in the hyperresolution chain. Thus, in the example, 59 is the nucleus; applying binary resolution to its second literal and the first literal of clause 47 produces a new clause; and applying binary resolution again, this time between the third literal of the new clause and the first literal of 38, produces the final result.

Ignoring labels and secondary steps in Prover9 syntax, an instance of the hyperresolution rule is expressed as follows.

Clause Formula . [ hyper ( Nucleus , First1 , Satellite1 , Second1 , . . ., FirstN , SatelliteN , SecondN )]

For the translation to our extension of TPTP, we provide the logic program that implements the procedure and define the mapping.

thf ( prover9_hyperresolution , semantics , Formula , calculus ( hol )).

Here Formula defines the logical semantics of hyperresolution recursively, in terms of the same generic (binary) resolution procedure that was used to model the tactic in Vampire.

∀ S1 , S2 , R : hyperresolution ([ S1 , S2 ] , R ) ⇐ resolution ( S1 , S2 , R ). ∀ S1 , S2 , Ss , R : hyperresolution ([ S1 , S2 | Ss ] , R ) ⇐ ∃ R ': resolution ( S1 , S2 , R ') ∧ hyperresolution ([ R ' | Ss ] , R ).
Insofar as the sequence of clauses and the expected final formula are known, we can ignore the triples passed as additional info and entrust the backtracking search mechanism to find an appropriate application of hyperresolution (assuming one exists). Consequently, the encoding drops the conjunct selection guidance given by Prover9 and represents a more general problem, solvable directly by the definition given here.

Object-to meta-level lifting of disjunction in LEO-II

As a final example, we consider a two-level logic tactic in the theorem prover LEO-II. In particular, we consider the extcnf or pos tactic, which is responsible for lifting a disjunction from the object level to the meta level of the logic [START_REF] Sultana | Understanding LEO-II's proofs[END_REF]. The rule has the following definition:

C ∨ [A ∨ B] tt C ∨ [A] tt ∨ [B]
tt

The tool expresses the application of this rule natively in TPTP syntax as follows.

thf ( ClauseId , plain , Formula , inference ( extcnf_or_pos , [ status ( thm )] , [ SourceId ])).

It should be noted that atoms in LEO-II are labeled with either true or false using the TPTP notation F = $true. Once a substitution is applied, atoms can become more complex formulas. Concretely, this inference rule is used to translate the object-level disjunction into the clause-level one.

To provide the semantics of this rule, we use a higher-order logic formulation:

thf ( leo2_extcnf_or_pos , semantics , Formula , calculus ( hol )).

Here Formula supplies the following definition for the underlying semantics (using explicit quantifiers).

∀ ClauseId , SourceId : extcnf_or_pos ( ClauseId , SourceId )

⇐ (((∀ C : C ⇔ C = ) ∧ SourceId ) ⇒ ClauseId )
It is easily seen that using the additional axiom one can easily use any calculus for higher-order logic to prove this normalization rule.

Discussion and conclusion

Even when we restrict our attention to the community of resolution theorem provers, there are several different approaches to proof certification. Sutcliffe [START_REF] Sutcliffe | Semantic derivation verification: Techniques and implementation[END_REF] proposed using the proof derivations in the TSTP library as a skeleton, which one can use to reconstruct a proof (possibly with the help of theorem provers). The Dedukti proof certifier [START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF] is a universal proof certifier which was successfully used to certify proofs of the iProver resolution theorem prover [START_REF] Korovin | iprover-an instantiation-based theorem prover for first-order logic (system description)[END_REF]. The proof certifier closest to the approach presented in this paper is that of the system checkers [START_REF] Chihani | The proof certifier checkers[END_REF], which uses logic programming in order to encode inference rule semantics and to reconstruct proofs. checkers has been used to partially certify E's [START_REF] Schulz | System description: E 1.8[END_REF] proofs. While the first method is based on using theorem provers for filling in the missing semantics in TPTP proofs, the latter two systems are stem from a concrete effort to denote the semantics of different theorem provers using deterministic and non-deterministic approaches, respectively. This effort is normally made by a different team from that which implemented the theorem prover and which has the deepest knowledge about the actual semantics of its calculus. The approach which was taken in this paper tries to make this effort easier and more accessible to the implementers of theorem provers. First, the language used to denote the semantics is well known to the implementers as it is already used to input problems and to output proofs. Second, unlike the last two systems mentioned, the implementers have a high degree of flexibility to define the semantics and are not restricted by external notions such as efficient or effective translations. This indeed put at risk the ability to mechanize these definitions into an actual certifier for the system but as mentioned in the paper, the parts which cannot be mechanized as given can, at least, be used to bring mechanization closer with some further help, for example, by the certification team.

The aim of this proposal is to convince the implementers of theorem provers that even semi-formal semantics, which can easily be defined using the approach presented, are useful for the purpose of full certification of their provers. The implementers can thus control the effort required of them in order to generate the semantics. The examples given in this paper range from the minimal effort of specifying a simple set of axioms to the greater effort of defining a full translation. While the second can be used efficiently by any of the two systems described at the beginning of this section, the first method requires only minimal additional effort in order to be used for proof reconstruction by a system like checkers.

In conclusion, TPTP can serve as a format for specifying the semantics of proofs for various degrees of concreteness. By using the same format for both problems, proofs and semantics, implementers are encouraged to consider the semantics as part of the implementation effort. This effort can both serve as documentation of the internal calculus and as an implementation of the semantics which can be later used for proof checking.

Both Teyjus[START_REF] Nadathur | System description: Teyjus -A compiler and abstract machine based implementation of λProlog[END_REF] and ELPI[START_REF] Dunchev | A fast interpreter for λProlog[END_REF] are implementations of λProlog.

Acknowledgments. This work has been funded by the ERC Advanced Grant ProofCert.


Roberto Blanco

Dale Miller

To appear in EPTCS

Keywords:

We apply the foundational proof certificate (FPC) framework to the problem of designing high-level outlines of proofs. The FPC framework provides a means to formally define and check a wide range of proof evidence. A focused proof system is central to this framework and such a proof system provides an interesting approach to proof reconstruction during the process of proof checking (relying on an underlying logic programming implementation). Here, we illustrate how the FPC framework can be used to design proof outlines and then to exploit proof checkers as a means for expanding outlines into fully detailed proofs. In order to validate this approach to proof outlines, we have built the ACheck system that allows us to take a sequence of theorems and apply the proof outline "do the obvious induction and close the proof using previously proved lemmas".

Theorem plustotal :

forall N , nat N -> forall M , nat M -> exists S , plus N M S .

Introduction

Inference rules, as used in, say, Frege proofs (a.k.a. Hilbert proofs) are usually greatly restricted by limitations of human psychology and by what skeptics are willing to trust. Typically, checking the application of inference rules involves simple syntactic checks, such as deciding on whether or not two premises have the structure A and A ⊃ B and the conclusion has the structure B. The introduction of automation into theorem proving has allowed us to engineer inference steps that are more substantial and include both computation and search. In recent years, a number of proof theoretic results allow us to extend that literature from being a study of minuscule inference rules (such as modus ponens or Gentzen's introduction rules) to a study of large scale and formally defined "synthetic" inference rules. In this paper, we briefly describe the ACheck system in which we build and check proof outlines as combinations of such synthetic rules.

Consider the following inductive specification of addition of natural numbers

Define plus : nat -> nat -> nat -> prop by plus z N N ; plus ( s N ) M ( s P ) := plus N M P .

where z and s denote zero and successor, respectively. (Examples will be displayed using the syntax of the Abella theorem prover [START_REF] Baelde | Abella: A System for Reasoning about Relational Specifications[END_REF]: this syntax should be familiar to users of other systems, such as Coq.) When this definition is introduced, we should establish several properties immediately, e.g., that the addition relation is determinate and total.

Theorem plus0com : forall N , nat N -> plus N z N .

Theorem plusscom : forall M , nat M -> forall N , nat N -> forall P , plus M N P -> plus M ( s N ) ( s P ).

Theorem pluscom : forall N , nat N -> forall M , nat M -> forall S , plus N M S -> plus M N S .

These three lemmas have the same high-level proof outline: use the obvious induction invariant, apply some previously proved lemmas and the inductive hypothesis, and deal with any remaining case analysis.

The fact that many theorems can be proved by using induction-lemmas-cases is well-known and built into existing theorem provers. For example, the waterfall model of the Boyer-Moore prover [START_REF] Boyer | A Computational Logic[END_REF] proves such theorems in a similar fashion (but for inductive definitions of functions). Twelf [START_REF] Pfenning | System Description: Twelf -A Meta-Logical Framework for Deductive Systems[END_REF] can often prove that some relations are total and functional using a series of similar steps [START_REF] Schürmann | A Coverage Checking Algorithm for LF[END_REF]. The tactics and tacticals of LCF have been used to implement procedures that attempt to find proofs using these steps [START_REF] Wilson | Inductive Proof Automation for Coq[END_REF]. Finally,

Γ B i ⇓ Γ B 1 ∨ B 2 ⇓ Γ B[t/x] ⇓ Γ ∃x.B ⇓

Figure 2: Focusing annotations

It is meaningless to use Gentzen's sequent calculus to directly support proof automation. Consider, for example, attempting to prove the sequent Γ ∃x∃y[(p x y) ∨ ((q x y) ∨ (r x y))], where Γ contains, say, a hundred formulas. The search for a (cut-free) proof of this sequent can confront the need to choose from among a hundredand-one introduction rules. If we choose the right-side introduction rule, we will then be left with, again, a hundred-and-one introduction rules to apply to the premise. Thus, reducing this sequent to, say, Γ (q t s) requires picking one path of choices in a space of 101 4 choices.

These rules need no external information (in particular, any new variable y will work in the ∃ introduction rule). In these last two rules, the zone between ⇑ and contains a list of formulas. When there are no more invertible rules that can be applied to that first formula, that formula is moved to (i.e., stored in) the zone written as Γ, using the following store-left rule

C, Γ ⇑ Θ R Γ ⇑C, Θ R S l .
Finally, when the zone between the ⇑ and the is empty (i.e., all invertible inference rules have been completed), it is time to select a (possibly non-invertible) introduction rule to attempt. For that, we have the two decide rules

Γ, N ⇓ N E Γ, N ⇑ • • ⇑ E D l and Γ P ⇓ Γ ⇑ • • ⇑ P D r .
Although we cannot show all focused inference rules, we will present those that deal with the least Γ µB t ⇓ Notice that the right introduction rule is just an unfolding of the fixed point. There are two ways to treat the least fixed point on the left: one can either perform a store operation or one can do an induction using, in this case, the invariant S. The right premise of the induction rule shows that S is a prefixed point (i.e., BS ⊆ S). In general, supplying an invariant can be tedious so we shall also identify two admissible rules for unfolding (also on the left) and obvious induction, meaning that the invariant to use is nothing more than the immediately surrounding sequent as the invariant S. In the case of the obvious induction, the left premise sequent will be trivial.

Foundational proof certificates

The main idea behind using the foundational proof certificate (FPC) [START_REF] Chihani | Foundational proof certificates in first-order logic[END_REF] approach to defining proof evidence is that theorem provers output their proof evidence to some persistent memory (e.g., a file) and that independent and trustable proof checkers examine this evidence for validity. In order for such a scheme to work, the semantics of the output proof evidence must be formally defined. The FPC framework provides ways to formally define such proof semantics which is also executable when interpreted on top of a suitable logic engine.

There are four key ingredients to providing such a formal definition and they are all described via their relationship to focused proof systems. In fact, consider the following augmented versions of inference rules we have seen in the previous section.

Ξ 1 : Γ B i ⇓ ∨ e (Ξ 0 , Ξ 1 , i) Ξ 0 : Γ B 1 ∨ B 2 ⇓ Ξ 1 : Γ B[t/x] ⇓ ∃ e (Ξ 0 , Ξ 1 ,t) Ξ 0 : Γ ∃x.B ⇓
These two augmented rules contain two of the four ingredients of an FPC: the schema variable Ξ ranges over terms that denote the actual proof evidence comprising a certificate. The additional premises involve experts which are predicates that relate the concluding certificate Ξ 0 to a continuation certificate Ξ 1 and some additional information. The expert predicate for the disjunction can provide an indication of which disjunct to pick and the expert for the existential quantifier can provide an indication of which instance of the quantifier to use. Presumably, these expert predicates are capable of digging into a certificate and extracting such information. It is not required, however, for an expert to definitively extract such information. For example, the disjunction expert might guess both 1 and 2 for i: the proof checker will thus need to handle such non-determinism during the checking of certificates. Another ingredient of an FPC is illustrated by the augmented inference rules in Figure 3. The store-left (S l ) inference rule is augmented with an extra premise that invokes a clerk predicate which is responsible for computing an index l that is associated to the stored formula (here, C). The augmented decide-left (D l ) rule is given an extra premise that uses an expert predicate: that premise can be used to compute the index of the formula that is to be selected for focus. The indexing mechanism does not need to be functional (i.e., different formulas can have the same index) in which case the decide rule must also be interpreted as non-deterministic. In earlier work [START_REF] Chihani | Foundational proof certificates in first-order logic[END_REF], indexes have been identified with structures as diverse as formula occurrences and de Bruijn numerals. In this paper, the only role planned by indexes will be as the names given to lemmas and to hypotheses (i.e., formulas that are stored on the left using the S l inference rule).

Ξ 1 : l,C , Γ ⇑ Θ R store c (Ξ 0 , Ξ 1 , l) Ξ 0 : Γ ⇑C, Θ R S l Ξ 1 : Γ, l,N ⇓ N E decide e (Ξ 0 , Ξ 1 , l) Ξ 0 : Γ, l,N ⇑ • • ⇑ E D l
As indicated above, there are essentially three operations that we can perform to treat a least fixed point formula in the left-hand context. In fact, we shall expand these into the following four augmented inference rules.

1. The fixed point can be "frozen" in the sense that the store-left (S l ) rule is applied to it. As a result of such a store operation, the stored occurrence of the fixed point will never be unfolded and will not be the site of an induction. Such a frozen fixed point can only be used later in proof construction within an instance of the initial rule.

2. The fixed point can be unfolded just as it can be on the right-hand side of the sequent. (Unfolding on the left is a consequence of the more general induction rule.) The following augmented inference rule can be used to control when such a fixed point is unfolded.

Ξ 1 : N ⇑ B(µB) t, Γ R unfold(Ξ 0 , Ξ 1 ) Ξ 0 : N ⇑ µB t, Γ R 3.
The most substantial inference rule related to the least fixed point is the induction rule. In its most general form, this inference rule involves proving premises that involve an invariant. A proof certificate term Ξ 0 could include such an invariant explicitly and the following augmented rule could be used to extract and use that invariant.

Ξ 1 : N ⇑ S t, Γ R Ξ 2 ȳ : N ⇑ B S ȳ S ȳ ind(Ξ 0 , Ξ 1 , Ξ 2 , S) Ξ 0 : N ⇑ µB t, Γ R 4.
In general, it appears that invariants are often complex, large, and tedious structures to build and use. Thus, it is most likely that we need to develop a number of techniques by which invariants are not built directly but are rather implied by alternative reasoning principles. For example, the Abella theorem prover [START_REF] Baelde | Abella: A System for Reasoning about Relational Specifications[END_REF], allows the user to do induction not by explicitly entering an invariant but rather by performing a certain kind of guarded, circular reasoning. In the context of this paper, we consider, however, only one approach to specifying induction and that involves taking the sequent N ⇑ µB t, Γ R and abstracting out the fixed point expression to yield the "obvious" invariant Ŝ so that the premise N ⇑ S t, Γ R has an easy proof. As a result, only the second premise related to the induction rule needs to be proved. The following augmented rule is used to generate and check whether or not the obvious induction invariant can be used.

Ξ 1 ȳ : N ⇑ B Ŝ ȳ Ŝ ȳ obvious(Ξ 0 , Ξ 1 ) Ξ 0 : N ⇑ µB t, Γ R
An FPC definition is then a collection of the following: (i) the term constructors for the term encoding proof evidence (the Ξ schema variable above), (ii) the constructors for building indexes, and (iii) the definitions of predicates for describing how the clerks and experts behave in different inference rules. Given these definitions, we then check whether or not a sequent of the form Ξ : Γ B is provable. This latter check can be done using a logic programming engine since such an engine should support both unification and backtracking search (thereby allowing one to have a trade-off between large certificates with a great deal of explicit information and small certificates where details are elided and reconstructed as needed). In our own work, we have used both λ Prolog [START_REF] Miller | Programming with Higher-Order Logic[END_REF] and Bedwyr [START_REF]The Bedwyr system[END_REF] as that logic-based engine.

Certificate design

Imagine telling a colleague "The proof of this theorem follows by a simple induction and the three lemmas we just proved." You may or may not be correct in such an assertion since (a) the proposed theorem may not be provable and (b) the simple proof you describe may not exist. In any case, it is clear that there is a rather simple, high-level algorithm to follow that will search for such a proof. In this section, we translate that algorithm into an FPC.

Following the paradigm of focused proof systems for first-order logic, there is a clear, high-level outline to follow for doing proof search for cut-free proofs: first do all invertible inference rules and then, select a formula on which to do a series of non-invertible choices. This latter phase ends when one encounters invertible inference rules again or the proof ends. In the setting we describe here, there are two significant complicating features with which to be concerned.

Treating the induction rule. The invertible (⇑) phase is generally a place where no important choices in the search for a proof appear. When dealing with a formula that is a fixed point, however, this is no longer true. As described in the previous section, we treat that fixed point expression either by freezing (see also [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]), unfolding, or using an explicitly supplied invariant or the "obvious" induction.

Lemmas must be invoked. Although the focusing framework can work with any provable formula as a lemma, we shall only consider lemmas that are Horn clauses (for example, the lemmas at the end of Section 2). Consider applying a lemma of the form ∀ x[A 1 ⊃ A 2 ⊃ A 3 ] in proving the sequent Γ E. Since the formulas A 1 , A 2 , and A 3 are polarized positively, we can design the proof outline (simply by only authorizing fixed points to be frozen during this part of the proof) so that Γ ⇓ ∀ x[A 1 ⊃ A 2 ⊃ A 3 ] E is provable if and only if there is a substitution θ for the variables in the list of variables x such that θ A 1 and θ A 2 are in Γ and the sequent Γ, θ A 3 E is provable. The application of such a lemma is then seen as forward chaining: if the context Γ contains two atoms (frozen fixed points) then add a third.

The main issue that a certificate-as-proof-outline therefore needs to provide is some indication of what lemmas should be used during the construction of a proof. The following collections of supporting lemmas-starting from the least explicit to the most explicit-have been tested within our framework: (i) a bound on the number of lemmas that can be used to finish the proof; (ii) a list of possible lemmas to use in finishing the proof; and (iii) a tree of lemmas, indicating which lemmas are applied following the conjunctive structure of the remaining proof.

The proof checker

A direct and natural way to implement the FPC approach to proof checking is to use a logic programming language: by turning the augmented inference rules sideways, one gets logic programming clauses. In this way, the rule's conclusion becomes the head of the clause and the rule's premises become the body of the clause. When proof checking in (either classical or intuitionistic) first-order logic without fixed points, the λ Prolog programming language [START_REF] Miller | Programming with Higher-Order Logic[END_REF] is a good choice since its treatment of bindings allows for elegant and effective implementations of first-order quantification in formulas and of eigenvariables in proofs [START_REF] Chihani | Foundational proof certificates in first-order logic[END_REF]. When the logic itself contains fixed points, as is the case in this paper, λ Prolog is no longer a good choice: instead, a stronger logic that incorporates aspects of the closed world assumption is needed. In particular, the ACheck system has two parts. The first is a theorem prover; we have used Abella since it was easy to modify it for exporting theorems and certificates for use by the second part. The second part is the proof checker, FPCcheck, that verifies the output of a session of the theorem prover, suitably translated. This checker is written in the Bedwyr model checking system [START_REF]The Bedwyr system[END_REF] and is the new component underlying this particular paper: its code is available from https://github.com/proofcert/fpccheck. The documentation at that address explains where to find Bedwyr and our modified Abella system.

To illustrate here the kinds of examples available on the web page, the Abella theory files can have a ship command that is followed by a string describing a certificate to use to prove the proposed theorem: the checking of this certificate is shipped to the Bedwyr-based kernel for checking. In this particular case, the induction certificate constructor is given three arguments: the first is the maximal number of decides that can be used in the proof and the second and third are bounds on the number of unfoldings in the ⇑ and ⇓ phases respectively.

Theorem plus0com : forall N , is_nat N -> plus N zero N .

ship " ( induction 1 0 1) " . Theorem plusscom : forall M , is_nat M -> forall N , is_nat N -> forall P , plus M N P -> plus M ( succ N ) ( succ P ). ship " ( induction 1 0 1) " . Theorem pluscom : forall N , is_nat N -> forall M , is_nat M -> forall S , plus N M S -> plus M N S . ship " ( induction 2 1 0) " .

The bound on the number of decide rules (first argument) is also a bound on the number of lemmas that can be used on any given branch of the proof.

System architecture

Our system for producing and checking proof outlines follows a simple linear work-flow: first, state a theorem and obtain a proof outline, next, attempt to check the theorem with the outline given as a proof certificate. We have structured this process in three computation steps, involving a theorem prover, a translator, and a proof checker. Their roles are given here.

The theorem prover. An existing theorem prover is principally the source of the concrete syntax of definitions and theorems. It may not be directly involved in the work-flow, particularly if the proof language is extended to support ship tactics that enable the omission of detailed proof scripts. At the end of the phase a theorem file with all relevant definitions, theorem statements and proof scripts is obtained.

The translator. For each theorem prover, we need to furnish a translator that can convert the concrete syntax of the theorem prover into that of the proof checker. It may export explicit certificates given by the ship tactic or derive certificates automatically, possibly making use of proof scripts and execution traces in the theorem file. These translation facilities may be built into the theorem prover itself, or an instrumented version of it, thus encapsulating the first two stages. The translator outputs translation files usable directly by a general-purpose, universal proof checker.

The proof checker. The proof checker, as described in Section 5, implements a focused version of the µLJ logic in the Bedwyr model checking system, augmented to further implement the FPC framework. The translated theorems and their certificates plug into this kernel and constitute a full instantiation of the system, which Bedwyr can execute to verify that the certificates can be elaborated into complete proofs of their associated theorems.

Translators are the only addition needed to enable a new theorem prover to use the FPC framework. Such translators are free to implement sophisticated mechanisms to produce efficient certificates from proof scripts but, in fact, only a more shallow syntactic translation is strictly required: in this latter case, sophistication must be built into the FPC definitions. For the present study with the Abella interactive theorem prover, the translator has been integrated in an instrumented version of Abella, a system whose proximity with Bedwyr syntax is naturally well-suited to the approach.

The work-flow structure just described makes no explicit reference to the FPCs that could be shipped, constructed, and checked. These can conform to the definition of proof outlines used throughout this paper or be tailored to each specific problem. The translator module can choose to use proof outlines as the default, as is the case in our examples. It could also let a user of ship specify an FPC definition to be included in the resulting translation, or generate tentative certificates with rules involving other FPC definitions.

Conclusion

We have described a methodology for elaborating proof outlines using a framework for checking proof certificates. We have illustrated this approach with "simple inductive proofs" that are applicable in a wide range of situations involving inductively defined datatypes. We plan to scale and study significantly more complex examples in the near future. Finally, it would be interesting to see how our use of high-level descriptions of proofs and proof reconstruction might be related to the work of Bundy and his colleagues on proof plans and rippling [START_REF] Bundy | The use of explicit plans to guide inductive proofs[END_REF][START_REF] Bundy | Rippling: A Heuristic for Guiding Inductive Proofs[END_REF].

Figure 3 :

 3 Figure 3: Two augmented rules

TAC[START_REF] Baelde | Focused Inductive Theorem Proving[END_REF] attempts to follow such a procedure as well but in a rather fixed and inflexible fashion. In this paper, we present an approach to describing the simple rules that can prove a given lemma based on previously proved lemmas. Specifically, we define proof certificates that describe the structure of a proof outline that we expect and then we run a proof checker on that certificate to see if the certificate can be elaborated into a full proof of the lemma.2 A focused proof systemΓ B i Γ B 1 ∨ B 2 Γ B[t/x] Γ ∃x.BFigure 1: From the LJ calculusConsider the two introduction rules in Figure1. If one attempts to prove sequents by reading these rules from conclusion to premises, then these rules need either information from some external source (e.g., an oracle providing the i ∈ {1, 2} or the term t) or some implementation support for non-determinism (e.g., unification and backtracking search).

Focused proof systems address this explosion by organizing rules into two phases. For example, the rules in Figure1are written instead as Figure2. Here, the formula on which one is introducing a connective is marked with the ⇓: as a result, reducing the sequent Γ ∃x∃y[(p x y) ∨ ((q x y) ∨ (r x y))] ⇓ to Γ (q t s) ⇓ involves only those choices related to the formula marked for focus: no interleaving of other choices needs to be considered.While the ⇓ phase involves rules that may not be invertible, the ⇑ phase involves rules that must be invertible. For example, the left rules for ∨ and ∃ are invertible and their introduction rule is listed asΓ ⇑ B 1 , Θ R Γ ⇑ B 2 , Θ R Γ ⇑ B 1 ∨ + B 2 , Θ R Γ ⇑ [y/x]B, Θ R Γ ⇑ ∃x.B, Θ R

fixed point operator. Formally speaking, when we define a predicate, such as plus in the previous section, we are actually naming a least fixed point expression. In the case of plus, that expression isµλ Pλ nλ mλ p.(n = z ∧ m = p) ∨ ∃n ∃p .[n = (s n ) ∧ p = (s p ) ∧ (P n m p )].For the treatment of least fixed points, we follow the µLJ proof system and its focused variant[START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]. The treatment of least fixed point expressions in the ⇑ phase and the ⇓ phase is given by the three rulesµB t, Γ ⇑ Θ R Γ ⇑ µB t, Θ R Γ ⇑ S t, Θ N ⇑ BS x S x Γ ⇑ µB t, Θ N Γ B(µB) t ⇓

Acknowledgments: We thank anonymous reviewers and K. Chaudhuri for comments on a draft of this paper. This work was funded by the ERC Advanced Grant ProofCert.