Specification for process oriented applications tends to use languages that suffer from infinite, intractable or unpredictably irregular state spaces that thwart exhaustive searches by verification heuristics. However, conceptual schemas based on FOL, offer techniques for both integrating and verifying specifications in finite spaces. It is therefore of interest to transform process based specifications into conceptual schemata. Process oriented languages have an additional drawback in that reliable inputs to the integration of diverse specifications can result in unreliable outputs. This problem can more easily be addressed in a logic representation in which static and dynamic properties can be examined separately. The first part of the text describes a translation method from the process based language SDL, to first order logic. The usefulness of the method for industrial application has been demonstrated in an implementation. The method devised is sufficiently general for application to other languages with similar characteristics. Main contributions consist of: formalising the mapping of state transitions to event driven rules in dynamic entity-relationship schemas; analysing the complexity of various approaches to decomposing transitions; a conceptual representation of the source language that distinguishes meta- and object models of the source language and domain respectively. The second part of the text formally describes a framework for the integration of schemata that allows the exploration of their properties in relation to each other and to a set of integration assertions. The main contributions are the formal framework; an extension to conflicts between agents in a temporal action logic; complexity estimates for various integration properties. / QC 20101004

Με σκοπό την ενίσχυση του μαθήματος Τεχνητή Νοημοσύνη στο τμήμα Μηχανικών Η/Υ και Πληροφορικής της Πολυτεχνικής σχολής του Πανεπιστημίου Πατρών έχει δημιουργηθεί από την Ομάδα Τεχνητής Νοημοσύνης το πρωτότυπο για ένα Ευφυές Σύστημα Διδασκαλίας Τεχνητής Νοημοσύνης (ΣΔΤΝ). Το σύστημα αυτό, ανάμεσα στα άλλα, διδάσκει την Κατηγορηματική Λογική ως γλώσσα Αναπαράστασης Γνώσης και Αυτόματου Συλλογισμού. Πρόκειται για ένα σύστημα που προσαρμόζεται, επιτρέποντας στους φοιτητές να επιλέγουν οι ίδιοι τον ρυθμό και το επίπεδο μάθησης. Ένα από τα θέματα που διαπραγματεύεται το σύστημα είναι και η μετατροπή από προτάσεις φυσικής γλώσσας (ΦΓ) σε εκφράσεις Κατηγορηματικού Λογισμού Πρώτης Τάξεως (ΚΛΠΤ). Επειδή η διαδικασία αυτή δεν είναι αυτοματοποιήσιμη, ο φοιτητής δεν μπορεί να πάρει κάποια βοήθεια ή υπόδειξη από το σύστημα, κατά τη διάρκεια μιας τέτοιας άσκησης, πριν δώσει την τελική του απάντηση. Γι’ αυτό, στα πλαίσια του ΣΔΤΝ αποφασίστηκε να ενσωματωθεί μια επιπλέον δυνατότητα: να μετατρέπει εκφράσεις ΚΛΠΤ τις οποίες δημιουργεί ο φοιτητής, στην προσπάθειά του να λύσει μια τέτοια άσκηση, σε προτάσεις ΦΓ. Σκοπός της λειτουργίας αυτής είναι να χρησιμοποιηθεί σαν ανατροφοδότηση από το σύστημα στον φοιτητή, προκειμένου ο τελευταίος να αξιολογήσει την απάντησή του, πριν την καταθέσει σαν τελική απάντησή στην άσκηση. Για την υλοποίηση της παραπάνω δυνατότητας ξεκίνησε η ανάπτυξη ενός συστήματος βασισμένου σε κανόνες, του FOLtoNL (First Order Logic to Natural Language). Στόχος του συστήματος ήταν η επιτυχής μετατροπή εκφράσεων ΚΛΠΤ σε ΦΓ. Το FOLtoNL υλοποιήθηκε σε Jess, μια γλώσσα προγραμματισμού με κανόνες (γραμμένη εξ’ ολοκλήρου σε Java) και αξιολογήθηκε με βάση τα αποτελέσματά του σε ειδικά σχεδιασμένο σύνολο εκφράσεων ΚΛΠΤ. / To help teaching the course of Artificial Intelligence in Computer Engineering and Informatics Department of Patras University, a web-based intelligent tutoring system, called Artificial Intelligence Teaching System (AITS), was created. Among other things, AITS teaches Predicate Logic as a Knowledge Representation and Automated Reasoning language and is an adapting system, allowing students to choose themselves the teaching rate and level. One of the issues that AITS deals with is the conversion of natural language (NL) sentences into First-Order Logic (FOL) formulas. Given that this is a non-automated process, it is difficult to give some hints to the students-users during their effort to convert an “unknown” (to the system) NL sentence into a FOL formula. However, some kind of help could be provided, if the system could translate (after checking its syntax) the proposed by the student FOL formula into a NL sentence. The student then will be able to compare the initial NL sentence with the one that its FOL formula corresponds to. In this way, it is easier to see whether his/her proposed FOL formula is compatible with the given NL sentence and perhaps make some amendments, before submitting the final answer. FOLtoNL (First Order Logic to Natural Language) is a rule-based system that converts FOL formulas into NL in order to provide the functionality described above. It uses the expert systems approach alongside natural language processing aspects. FOLtoNL is implemented in Jess (an expert system shell written in Java) and has been evaluated via an appropriately created set of FOL expressions.

Les réseaux biologiques, notamment les réseaux de signalisation déclenchés par les hormones, sont extrêmement complexes. Les méthodes expérimentales à haut débit permettent d’aborder cette complexité, mais la prise en compte de l’ensemble des données générées requiert la mise au point de méthodes automatiques pour la construction des réseaux. Nous avons développé une nouvelle méthode d’inférence reposant sur la formalisation, sous forme de règles logiques, du raisonnement de l’expert sur les données expérimentales. Cela nécessite la constitution d’une base de connaissances, ensuite exploitée par un moteur d’inférence afin de déduire les conclusions permettant de construire les réseaux. Notre méthode a été élaborée grâce au réseau de signalisation induit par l’hormone folliculo-stimulante dont le récepteur fait partie de la grande famille des récepteurs couplés aux protéines G. Ce réseau a également été construit manuellement pour évaluer notre méthode. Un contrôle a ensuite été réalisé sur réseau induit par le facteur de croissance épidermique, se liant à un récepteur tyrosine kinase, de façon à montrer que notre méthode est capable de déduire différents types de réseaux de signalisation. / Biological networks, including signalling networks induced by hormones, are very complex. High-throughput experimental methods permit to approach this complexity, but to be able to use all generated data, it is necessary to create automatical inference methods to build networks. We have developped a new inference method based on the formalization of the expert’s reasoning on experimental data. This reasoning is converted into logical rules. This work requires the creation of a knowledge base which is used by an inference engine to deduce conclusions to build networks. Our method has been elaborated by the construction of the signalling network induced by the follicle stimulating hormone whose receptor belongs to the G protein-coupled receptors family. This network has also been built manually to assess our method. Then, a test has been done on the network induced by the epidermal growth factor, which binds to a tyrosine kinase receptor, to demonstrate the ability of our method to deduce differents types of signaling networks.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Orientador: Itala Maria Loffredo D'Ottaviano / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-22T15:04:13Z (GMT). No. of bitstreams: 1 Almeida_EdgarLuisBezerrade_M.pdf: 946200 bytes, checksum: e8e316a3ee7420c8d7f45a751651a436 (MD5) Previous issue date: 2013 / Resumo: Esta Dissertação apresenta uma definição de lógica abstrata e caracteriza alguns sistemas lógicos bastante conhecidos na literatura como casos particulares desta. Em especial, mostramos que a lógica de primeira ordem, lógica de segunda ordem, lógica com o operador Q1 de Mostowski e a lógica infinitária L!1! são casos particulares de lógicas abstratas. Mais que isso, mostramos que tais lógicas são regulares. Na análise de cada uma das lógicas acima citadas, mostramos o comportamento das mesmas com relação às propriedades de Löwenheim-Skolem e compacidade enumerável, resultados estes centrais à teoria de modelos. Nossa análise permite-nos constatar que, dentre os quatro casos apresentados, o único que goza de ambas as propriedades é a lógica de primeira ordem; as demais falham em uma, na outra ou em ambas as propriedades. Mostramos que isso não é mera coincidência, mas sim um resultado profundo, que estabelece fronteiras bem delimitadas à lógica de primeira ordem, conhecido como primeiro teorema de Lindström: se uma lógica é regular, ao menos tão expressiva quanto à lógica de primeira ordem e satisfaz ambas as propriedades citadas, então esta é equivalente a lógica de primeira ordem. Realizamos uma prova cuidadosa do teorema, em que cada ideia e cada estratégia de prova é estabelecida criteriosamente. Com seu trabalho, Lindström inaugurou um novo e profícuo campo de estudo, a teoria abstrata de modelos que estabelece, com relação a diversas combinações de propriedades de sistemas lógicos, uma estratificação entre lógicas. Apresentamos um outro exemplo de tal estratificação através de uma versão modal do teorema de Lindström, versão esta que caracteriza a lógica modal básica como maximal quanto a bissimilaridade e compacidade. Encerramos esta Dissertação com algumas considerações acerca da influência do primeiro teorema de Lindström / Abstract: This thesis presents the definition of abstract logic and features some quite logical systems presented in the literature as particular cases of this. In particular, we show that first-order logic, second-order logic, the logic with Mostowski's operator Q1 and the infinitary logic L!1! are specific systems of abstract logic. Moreover, we show that such logics are regular. In the analysis of each above mentioned logical systems we analyses his performance with regard to the properties of compactness and Löwenheim-Skolem, results that have important role in model theory. Our analysis allows us to conclude that among the four cases, the only one who enjoys both properties is the first-order logic, and all others fail in one, other or both properties. We show that this is not mere coincidence, but rather a deep, well-defined boundaries establishing the first-order logic, known as first Lindström's theorem: a regular logic that is at least as expressive as first-order logic and satisfies both properties mentioned, then this is equivalent to first-order logic. We conducted a thorough proof of the theorem, in which each idea and each proof strategy is carefully established. With his work Lindström inaugurated a new and fruitful field of study, the abstract model theory, which establishes with respect to different combinations of properties of logical systems, stratification between logical. Here is another example of such stratification through one of the theorem of modal version Lindström, which characterizes this version of the logic basic modal such as maximal bissimimulation and compactness. We conclude the thesis with some considerations about the influence of the Lindström's theorem / Mestrado / Filosofia / Mestre em Filosofia

The increasing use of model-driven software development has renewed emphasis on using domain-specific models during application development. More specifically, there has been emphasis on using domain-specific modeling languages (DSMLs) to capture user-specified requirements when creating applications. The current approach to realizing these applications is to translate DSML models into source code using several model-to-model and model-to-code transformations. This approach is still dependent on the underlying source code representation and only raises the level of abstraction during development. Experience has shown that developers will many times be required to manually modify the generated source code, which can be error-prone and time consuming. An alternative to the aforementioned approach involves using an interpreted domain-specific modeling language (i-DSML) whose models can be directly executed using a Domain Specific Virtual Machine (DSVM). Direct execution of i-DSML models require a semantically rich platform that reduces the gap between the application models and the underlying services required to realize the application. One layer in this platform is the domain-specific middleware that is responsible for the management and delivery of services in the specific domain. In this dissertation, we investigated the problem of designing the domain-specific middleware of the DSVM to facilitate the bifurcation of the semantics of the domain and the model of execution (MoE) while supporting runtime adaptation and validation. We approached our investigation by seeking solutions to the following sub-problems: (1) How can the domain-specific knowledge (DSK) semantics be separated from the MoE for a given domain? (2) How do we define a generic model of execution (GMoE) of the middleware so that it is adaptable and realizes DSK operations to support delivery of services? (3) How do we validate the realization of DSK operations at runtime? Our research into the domain-specific middleware was done using an i-DSML for the user-centric communication domain, Communication Modeling Language (CML), and for microgrid energy management domain, Microgrid Modeling Language (MGridML). We have successfully developed a methodology to separate the DSK and GMoE of the middleware of a DSVM that supports specialization for a given domain, and is able to perform adaptation and validation at runtime.

<p>Many computer systems in our daily life require highly available applications (such as medical equipment) and some others run on difficult to access places (such as satellites). These systems are subject to a variety of potential failures that may degrade their performance. Therefore, being able to reason about faults and their impact on systems is gaining considerable attention. Existing work on fault tolerance is mostly focused on addressing faults at the programming language level. In the recent past, significant efforts have been made to use formal methods to specify and verify fault tolerant systems to provide more reliable software. Related with this, some researchers have pointed out that Deontic Logic is useful for reasoning about fault tolerant systems due to its expressive nature in relation to defining norms, used to describe expected behaviour and prescribing what happens when these norms are violated.</p> <p>In this thesis, we demonstrate how Deontic Logic can be used to model an existing real world problem concerning fault tolerance mechanisms. We consider different situations that a vehicle faces on the road and the consequent reactions of the driver or vehicle based on good and bad behaviour. We got the idea and motivation for this case study from the SASPENCE sub-project, conducted under the European Integrated Project PReVENT. This sub-project focuses on a vehicle’s behaviour in maintaining safe speed and safe distance on the road. As our first modelling attempt, we use a Propositional Deontic Logic approach, to justify to what extent we can apply this Logical approach to model a real world problem. Subsequently, we use a First Order Deontic Logic approach, as it can incorporate the use of parameters and quantification over them, which is more useful to model real world scenarios.</p> <p>We state and prove some interesting expected properties of the models using a First Order proof system. Based on these modelling exercises, we acquired different engineering ideas and lessons, and present them in this thesis in order to aid modelling of future fault tolerant systems.</p> / Master of Science (MSc)

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1. / text