Logical frameworks allow us to specify formal systems and prove properties about them. One interesting logical framework is Twelf, a language that uses higher order abstract syntax to encode object languages into the meta language. Currently, uniform proofs have been used for describing proof search in backwards logic programming style. However, there are certain limitations to a backward system, for example, loop-detection mechanisms are required for some of the simplest problems to yield a solution. As a consequence, the search for a more effective proof search algorithm prevails and a forward system is proposed. This thesis will discuss the theoretical foundations for a forward uniform sequent calculus and the implementation of an inverse method prover for Twelf. / Les cadres logiques nous permettent de spécifier des systèmes formels et de prouver des propriétés à leur sujet. Un cadre logique intéressant est Twelf, un langage qui emploie la syntaxe abstraite d'ordre supérieur pour encoder des langages objet dans le méta-langage. Actuellement, nous employons des preuves uniformes pour décrire la recherche dans le style de programmation logique arrière. Cependant, il y a certaines limitations à un système arrière: des mécanismes de détection de boucle sont nécessaires pour trouver une solution à certains des problèmes les plus simples. Par conséquent, la recherche d'un algorithme plus efficace de recherche de preuve règne et un système vers l'avant est proposé. Cette thèse discutera les bases théoriques d'un calcul séquent uniforme vers l'avant et l'implantation d'un prouveur à méthode inverse pour Twelf.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QMM.18796 |
| Date | January 2008 |
| Creators | Li, Xi |
| Contributors | Brigitte Pientka (Supervisor) |
| Publisher | McGill University |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Coverage | Master of Science (School of Computer Science) |
| Rights | All items in eScholarship@McGill are protected by copyright with all rights reserved unless otherwise indicated. |
| Relation | Electronically-submitted theses. |
Page generated in 0.0023 seconds