Rozprawy doktorskie na temat „Predicate calculus”

Le typage permet d'apporter de la sûreté dans la programmation, et il est utilisé au coeur de la majorité des systèmes de preuve. Plus un système de types est expressif, plus il est aisé d'y encoder des invariantsqui seront vérifiés mécaniquement lors du typage. Les types dépendants sont une extension des types simples dans laquelle les types peuvent dépendre de valeurs. Ils permettent par exemple de définir les vecteurs paramétrés par leur longueur. Le sous-typage par prédicat est une autre extension des types simples, dans laquelle les types peuvent être définis par des prédicats. Un sous-type défini par un prédicat, généralement noté { x : A | P(x) }, est habité par les éléments t de type A pour lesquels P(t) est vrai. Cette extension fournit un système de type très riche et intuitif, mais qui rend le typage indécidable.Cet ouvrage est dédié à l'encodage du sous-typage par prédicats dans Dedukti, un cadre logique avec des règles de calcul. On commence par encoder une version explicite du sous-typage par prédicats pour lequel un habitant de { x: A | P(x) } est syntaxiquement différent d'un habitant de A. On montre que tout jugement dérivable dans cette version du sous-typage par prédicat peut être encodé en un jugement dérivable du cadre logique.Le sous-typage par prédicat est souvent utilisé de manière implicite, sans différence syntaxique entre les habitants de A et les habitants de { x: A | P(x) }. On enrichit le cadre logique avec un système de raffinement des termes qui pourra ajouter ces marqueurs syntaxiques. Ce raffineur peut traduire des jugements typables avec du sous-typage par prédicat implicite en des jugements typable avec du sous-typage explicite.L'assistant à la preuve pvs utilise abondamment le sous-typage par prédicat. On montre comment sa bibliothèque standard peut être exportée vers Dedukti. Par ailleurs, PVS ne préserve que des traces de preuves. Dans la pénultième section, on décrit une procédure pour générer des preuves complètes à partir des traces laissées par PVS.La dernière section détaille une architecture pour l'entrepôt et l'échange de preuves formelles, afin de promouvoir l'interopérabilité
Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Dependent types extend simple types by allowing types to depend on values. For instance, it allows to define the types of lists of a certain length. Predicate subtyping is another extension of simple type theory in which types can be defined by predicates. A predicate subtype, usually noted {x: A | P(x)}, is inhabited by elements t of type A for which P(t) is true. This extension provides an extremely rich and intuitive type system, which is at the heart of the proof assistant PVS, at the cost of making type checking undecidable.This work is dedicated to the encoding of predicate subtyping in Dedukti: a logical framework with computation rules. We begin with the encoding of explicit predicate subtyping for which the terms in {x: A | P(x)} and terms of Aare syntactically different. We show that any derivable judgement of predicate subtyping can be encoded into a derivable judgement of the logical framework. Predicate subtyping, is often used implicitly: with no syntactic difference between terms of type A and terms of type {x: A | P(x) }. We enrich our logical framework with a term refiner which can add these syntactic markers. This refiner can be used to refine judgements typed with implicit predicate subtyping into explicited judgements.The proof assistant PVS uses extensively predicate subtyping. We show how its standard library can be exported to Dedukti. Because PVS only store proof traces rather than complete proof terms, we sketch in the penultimate section a procedure to generate complete proof terms from these proof traces.The last section provides the architecture of a repository dedicated to the exchange of formal proofs. The goal of such a repository is to categorise and store proofs encoded in Dedukti to promote interoperability

In this thesis we propose the use of Dijkstra's concept of a predicate transformer [Dij75] for the determination of database transaction safety [SS89] and the generation of simple conditions to check that a transaction will not violate the integrity constraints in the case that it is not safe. The generation of this simple condition is something that can be done statically, thus providing a mechanism for generating safe transactions. Our approach treats a database as state, a database transaction as a program, and the database's integrity constraints as a postcondition in order to use a predicate transformer [Dij75] to generate a weakest precondition. We begin by introducing a set-oriented update language for relational databases for which a predicate transformer is then defined. Subsequently, we introduce a more powerful update language for deductive databases and define a new predicate transformer to deal with this language and the more powerful integrity constraints that can be expressed using recursive rules. Next we introduce a data model with object-oriented features including methods, inheritance and dynamic overriding. We then extend the predicate transformer to handle these new features. For each of the predicate transformers, we prove that they do indeed generate a weakest precondition for a transaction and the database integrity constraints. However, the weakest precondition generated by a predicate transformer still involves much redundant checking. For several general classes of integrity constraint, including referential integrity and functional dependencies, we prove that the weakest precondition can be substantially further simplified to avoid checking things we already know to be true under the assumption that the database currently satisfies its integrity con-straints. In addition, we propose the use of the predicate transformer in combination with meta-rules that capture the exact incremental change to the database of a particular transaction. This provides a more general approach to generating simple checks for enforcing transaction safety. We show that this approach is superior to known existing previous approaches to the problem of efficient integrity constraint checking and transaction safety for relational, deductive, and deductive object-oriented databases. Finally we demonstrate several further applications of the predicate transformer to the problems of schema constraints, dynamic integrity constraints, and determining the correctness of methods for view updates. We also show how to support transactions embedded in procedural languages such as C.

In this thesis we propose the use of Dijkstra's concept of a predicate transformer [Dij75] for the determination of database transaction safety [SS89] and the generation of simple conditions to check that a transaction will not violate the integrity constraints in the case that it is not safe. The generation of this simple condition is something that can be done statically, thus providing a mechanism for generating safe transactions. Our approach treats a database as state, a database transaction as a program, and the database's integrity constraints as a postcondition in order to use a predicate transformer [Dij75] to generate a weakest precondition. We begin by introducing a set-oriented update language for relational databases for which a predicate transformer is then defined. Subsequently, we introduce a more powerful update language for deductive databases and define a new predicate transformer to deal with this language and the more powerful integrity constraints that can be expressed using recursive rules. Next we introduce a data model with object-oriented features including methods, inheritance and dynamic overriding. We then extend the predicate transformer to handle these new features. For each of the predicate transformers, we prove that they do indeed generate a weakest precondition for a transaction and the database integrity constraints. However, the weakest precondition generated by a predicate transformer still involves much redundant checking. For several general classes of integrity constraint, including referential integrity and functional dependencies, we prove that the weakest precondition can be substantially further simplified to avoid checking things we already know to be true under the assumption that the database currently satisfies its integrity con-straints. In addition, we propose the use of the predicate transformer in combination with meta-rules that capture the exact incremental change to the database of a particular transaction. This provides a more general approach to generating simple checks for enforcing transaction safety. We show that this approach is superior to known existing previous approaches to the problem of efficient integrity constraint checking and transaction safety for relational, deductive, and deductive object-oriented databases. Finally we demonstrate several further applications of the predicate transformer to the problems of schema constraints, dynamic integrity constraints, and determining the correctness of methods for view updates. We also show how to support transactions embedded in procedural languages such as C.
Thesis (PhD Doctorate)
Doctor of Philosophy (PhD)
School of Computing and Information Technology
Faculty of Information and Communication Technology
Full Text

Submitted by Aelson Maciera (aelsoncm@terra.com.br) on 2017-08-25T18:53:26Z No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5)
Approved for entry into archive by Ronildo Prado (bco.producao.intelectual@gmail.com) on 2018-01-24T12:17:05Z (GMT) No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5)
Approved for entry into archive by Ronildo Prado (bco.producao.intelectual@gmail.com) on 2018-01-24T12:18:07Z (GMT) No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5)
Made available in DSpace on 2018-01-24T12:21:46Z (GMT). No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5) Previous issue date: 2017-05-05
Não recebi financiamento
The purpose of this work is to propose a method that allow to bring the fundamentals of mathematical logic to high school through the use of set theory, however making the whole approach of the subject through diagrams, making it possible to avoid, for the demonstrations and understanding necessary to the development of the subject, the rigors of writing used in mathematical logic, which, in a first contact, tend to discourage the interest of beginning students.
O objetivo deste trabalho é propor um método que permita levar os fundamentos da lógica matemática para o ensino médio por meio da utilização da teoria dos conjuntos, porém fazendo todo a aproximação do assunto utilizando diagramas, tornando possível evitar assim, para as demonstrações e o entendimento necessários ao desenvolvimento do assunto, os rigores da escrita utilizada na lógica matemática, que, em um primeiro contato, podem desestimular o interesse dos alunos iniciantes

Doktorska disertacija prezentuje nov i opštiji način analiziranja semantike strukturiranih i objektno orijentisanih programa i to isključivo u okvirima predikatske logike prvog reda. Doktorska disertacija razmatra sledeće teme:1.) S-programski račun,2.) Definicija i osobine dinamičkih postuslova u S-računu,3.) Konceptualne definicije objekta, klase i invarijante,4.) Analiza invarijanata u klasi (SP-analiza i DP-analiza).
Doctoral thesis presents a new and more general method for analizing of structured and object-oriented program semantics, based on the first-order predicate logic. Doctoral thesis consideres next topics:1.) S-program calculus,2.) Definition and characteristics of dynamic postconditions in S-calculus,3.) Conceptual definitions of object, class and invariant,4.) Analyses of invariants in class (SP-analyses and DP-analyses).

Made available in DSpace on 2016-04-27T17:27:11Z (GMT). No. of bitstreams: 1 Cassia Sampaio Sanctos.pdf: 875084 bytes, checksum: 3baa23ce43e41c748fa70bf983f30e20 (MD5) Previous issue date: 2015-05-11
Coordenação de Aperfeiçoamento de Pessoal de Nível Superior
The thesis constitutes a critical review of Gödel´s doctoral dissertation which presents a proof for the completeness of first order logic. The introduction addresses the concepts of formalism, axiomatic method and completeness, thus the proof can be contextualized. The language for the restricted functional calculus is defined, with the corresponding syntax and semantics, and the original Gödel´s demonstration is updated. The appendix contains a translation of the referred dissertation, which is unprecedented in Portuguese
O trabalho constitui um comentário crítico da dissertação de doutorado de Gödel que apresenta uma prova de completude da lógica de primeira ordem. A introdução trata dos conceitos de formalismo, método axiomático e completude, para que seja possível contextualizar a prova. A linguagem para o cálculo funcional restrito é definida, com sua sintaxe e semântica, e a demonstração original de Gödel é atualizada. O apêndice contém a tradução da referida dissertação, que é inédita em língua portuguesa

Le but de ce travail consiste a etendre au calcul des predicats la methode de resolution pour la logique propositionnelle modale qui a ete definie par m. Luis farinas del cerro. Le systeme modal considere, appele q, est un sous-systeme de ceux plus connus, t, s4 et s5. Nous considerons toutefois que les resultats obtenus dans ce travail peuvent facilement etre etendus a ceux-ci. Nous definissons une propriete de herbrand modale pour le systeme q et en donnons la preuve. Cette propriete nous permet ensuite de definir un systeme de regles de resolution dans lequel l'unification des termes est soumise a certaines restrictions, et d'en prouver sa correction et sa completude

Rappel sur la logique mathematique et ses applications dans le domaine des languages predicatifs. Rappel sur les languages de base de donnees et de leurs principes fondamentaux. Si l'on trouve les memes principes elementaires par courbe en ce qui concerne les techniques d'optimisation, elles different d'un systeme a l'autre. Presentation de la syntaxe du language et du traitement general. Il est montre comment les algorithmes decrits peuvent etre repris dans le cadre du language pascal objet relationnel

Hoare and He's Unifying Theories of Programming (UTP) provides a rich model of programs as relational predicates. This theory is intended to provide a single framework in which any programming paradigms, languages, and features, can be modelled, compared and contrasted. The UTP already has models for several programming formalisms, such as imperative programming, higher-order programming (e.g. programing with procedures), several styles of concurrent programming (or reactive systems), class-based object-orientation, and transaction processing. We believe that the UTP ought to be able to represent all significant computer programming language formalisms, in order for it to be considered a unifying theory. One gap in the UTP work is that of object-based object-orientation, such as that presented in Abadi and Cardelli's untyped object calculi (sigma-calculi). These sigma-calculi provide a prominent formalism of object-based object-oriented (OO) programs, which models programs as objects. We address this gap within this dissertation by presenting an embedding of an Abadi--Cardelli-style object calculus in the UTP. More formally, the thesis that his dissertation argues is that it is possible to provide an object-based object rientation to the UTP, with value- and reference-based objects, and a fully abstract model of references. We have made three contributions to our area of study: first, to extend the UTP with a notion of object-based object orientation, in contrast with the existing class-based models; second, to provide an alternative model of pointers (references) for the UTP that supports both value-based compound values (e.g. objects) and references (pointers), in contrast to existing UTP models with pointers that have reference-based compound values; and third, to model an Abadi-Cardelli notion of an object in the UTP, and thus demonstrate that it can unify this style of object formalism.

Presentation des diverses methodes de traitement de requetes recursives. Des strategies d'optimisation sont etudiees et plusieurs facteurs influant les performances des methodes de traitement de requetes recursives sont mis en evidence. Une methode de traitement de requetes manipulant des relations virtuelles est proposee

Presentation du langage pascal/relationnel construit a partir de pascal par adjonction de constructions venant du domaine des bases de donnees ainsi que la conception et l'implantation du traducteur du langage. Les instructions relationnelles sont inspirees du calcul des predicats et permettent les operations classiques offertes par les systemes de gestion de bases de donnees relationnelles

Cette thèse se propose d’aborder la question de la causalité dans une perspective formelle inspirée du cadre de la SDRT (Segmented Discourse Representation Theory). Elle prête en particulier attention aux expressions paratactiques de la relation de causalité. Cette approche nous paraît intéressante et féconde par l’approche formaliste qu’elle met en œuvre, son objet étant particulièrement labile. L’analyse, dans ce travail, est notamment centrée sur l’expression linguistique des relations causales. L’approche adoptée, pour mener à bien les traitements, est dans une large mesure de nature sémantico-pragmatique. Bien que le fonctionnement de la causalité marquée linguistiquement, notamment au moyen de parce que, soit particulièrement documenté dans le paysage scientifique (Moeschler 2003, Rossari 2004, Knott 1996, etc), les enchaînements non marqués (paratactiques) semblent être peu étudiés dans les recherches linguistiques. Ce qui constitue en quelque sorte la motivation principale qui a impulsé la mise en œuvre de cette monographie. Cette étude pourrait donc se situer à l’interface entre linguistique théorique et linguistique formelle. Les traitements qui y sont effectués prennent appui dans une large part sur le corpus EXPLICADIS (Explication et Argumentation en Discours). Le choix de cette ressource pourrait se justifier de la sorte : ce corpus permet de rendre compte des relations causales selon une approche sémasiologique consistant à s’appuyer presque exclusivement sur la relation elle-même sans tenir compte de ses marqueurs linguistiques. Par ailleurs, nous aborderons, dans cette recherche, la question de la Causation. Sur ce plan, le traitement argumental (« Le spectre argumental ») des verbes dits causatifs (causer, provoquer, déclencher, etc.) nous permettrait de noter que les arguments de ce type particulier de prédicats admettraient une interprétation propositionnelle. L’hypothèse de départ est que la causation, ainsi conçue, semble représenter une relation inter-propositionnelle implicite ou plus simplement sous-jacente. Bien plus, nous nous intéresserons à la dichotomie causalité / agentivité
This thesis proposes to address the question of causality in a formal perspective inspired by the framework of SDRT (Segmented Discourse Representation Theory). In particular, she pays attention to paratactic expressions of the causal relationship. This approach seems interesting and fruitful to us by the formalistic approach that it implements, its object being particularly labile. The analysis in this work focuses on the linguistic expression of causal relationships. The approach adopted to carry out treatments is to a large extent semantico-pragmatic. Although the functioning of linguistically marked causality, especially by means of because, is particularly documented in the scientific landscape (Moeschler 2003, Rossari 2004, Knott 1996, etc.), untagged sequences (paratactic) seem to be little studied in the linguistic research. This is in a way the main motivation that drove the implementation of this monograph. This study could therefore be situated at the interface between theoretical linguistics and formal linguistics. The treatments that are carried out rely largely on the EXPLICADIS corpus (Explanation and Speech argumentation). The choice of this resource could be justified in this way: this corpus makes it possible to account for causal relations according to a semasiological approach of relying almost exclusively on the relation itself without taking into account its linguistic markers.Moreover, we will address, in this research, the question of the Causation. In this respect, the argumental treatment ("the speculative spectrum") of so-called causative verbs (cause, provoke, trigger, etc.) would allow us to note that the arguments of this particular type of predicate would admit a propositional interpretation. The initial hypothesis is that the causation, thus conceived, seems to represent an implicit or more simply underlying inter-propositional relation. Moreover, we will focus on the causality / agency dichotomy

In this dissertation we prove the Completeness, Soundness and Compactness of the Monadic Hybrid Calculus MHC and we prove its expressive equivalence to the Monadic Predicate Calculus MPC. The Monadic Hybrid Calculus MHC is a new system that is based on the (propositional) modal logic S5. It is “Hybrid” in the sense that it includes quantifier free MPC and therefore, unlike S5, allows free individual constants. The main innovation in this system is the elimination of bound variables. In MHC, upper case letters denote properties and lower case letters denote individuals. Universal quantification is represented by square brackets, [], and existential quantification is represented by angled brackets, 〈〉. Thus, All Athenians are Greek and mortal is formalized as [A](G∧M), Some mortal Greeks are Athenians as 〈M∧G〉A, and Socrates is mortal and Athenian as s(M∧A). We give the formal syntax and the formal semantics of [MHC] and give Beth-style Tableau Rules (Inference Rules). In these rules, if [P]Q is on the right then we select a new constant [v] and we add [vP] on left, vQ on the right, and we cancel the formula. If [P]Q is on the left then we select a pre-used constant p and split the tree. We add pP on the right of one branch and pQ on the left of the other branch. We treat 〈P〉Q similarly. Our Completeness proof uses induction on formulas down a path in the proof tree. Our Soundness proof uses induction up a path. To prove that MPC is logically equivalent to the Monadic Predicate Calculus, we present algorithms that transform formulas back and forth between these two systems. Compactness follows immediately. Finally, we examine the pragmatic usage of the Monadic Hybrid Calculus and we compare it with the Monadic Predicate Calculus using natural language examples. We also examine the novel notions of the Hybrid Predicate Calculus along with their pragmatic implications.
Graduate
0800
0984

Με σκοπό την ενίσχυση του μαθήματος Τεχνητή Νοημοσύνη στο τμήμα Μηχανικών Η/Υ και Πληροφορικής της Πολυτεχνικής σχολής του Πανεπιστημίου Πατρών έχει δημιουργηθεί από την Ομάδα Τεχνητής Νοημοσύνης το πρωτότυπο για ένα Ευφυές Σύστημα Διδασκαλίας Τεχνητής Νοημοσύνης (ΣΔΤΝ). Το σύστημα αυτό, ανάμεσα στα άλλα, διδάσκει την Κατηγορηματική Λογική ως γλώσσα Αναπαράστασης Γνώσης και Αυτόματου Συλλογισμού. Πρόκειται για ένα σύστημα που προσαρμόζεται, επιτρέποντας στους φοιτητές να επιλέγουν οι ίδιοι τον ρυθμό και το επίπεδο μάθησης. Ένα από τα θέματα που διαπραγματεύεται το σύστημα είναι και η μετατροπή από προτάσεις φυσικής γλώσσας (ΦΓ) σε εκφράσεις Κατηγορηματικού Λογισμού Πρώτης Τάξεως (ΚΛΠΤ). Επειδή η διαδικασία αυτή δεν είναι αυτοματοποιήσιμη, ο φοιτητής δεν μπορεί να πάρει κάποια βοήθεια ή υπόδειξη από το σύστημα, κατά τη διάρκεια μιας τέτοιας άσκησης, πριν δώσει την τελική του απάντηση. Γι’ αυτό, στα πλαίσια του ΣΔΤΝ αποφασίστηκε να ενσωματωθεί μια επιπλέον δυνατότητα: να μετατρέπει εκφράσεις ΚΛΠΤ τις οποίες δημιουργεί ο φοιτητής, στην προσπάθειά του να λύσει μια τέτοια άσκηση, σε προτάσεις ΦΓ. Σκοπός της λειτουργίας αυτής είναι να χρησιμοποιηθεί σαν ανατροφοδότηση από το σύστημα στον φοιτητή, προκειμένου ο τελευταίος να αξιολογήσει την απάντησή του, πριν την καταθέσει σαν τελική απάντησή στην άσκηση. Για την υλοποίηση της παραπάνω δυνατότητας ξεκίνησε η ανάπτυξη ενός συστήματος βασισμένου σε κανόνες, του 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.

碩士
高雄醫學大學
醫學研究所
100
Objectives To assess the effects of abdominal fat on shock wave lithotripsy (SWL). We used pre-SWL unenhanced computed tomography (CT) to evaluate the impact of abdominal fat distribution and calculus characteristics on the outcome of SWL. Methods One hundred and eighty-five patients with a solitary ureteric calculus treated with SWL were retrospectively reviewed. Each patient underwent unenhanced CT within 1 month before SWL treatment. Treatment outcomes were evaluated 1 month later. Unenhanced CT parameters, including calculus surface area, Hounsfield unit (HU) density, abdominal fat area and skin to calculus distance (SSD) were analyzed. Results One hundred and twenty-eight of the 185 patients were found to be calculus-free following treatment. HU density, total fat area, visceral fat area, and SSD were identified as significant variables on multivariate