NDLTD logo NDLTD Union Catalog and Global ETD Search

Global ETD Search

Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.

Results

Showing 1 to 15 of 15 for “"higher-order logic"”.

  1. A Resolution Style Proof Procedure for Higher-Order Logic

    Henschen, Lawrence JosephUniversity of Illinois at Urbana-Champaign2014

    Made available in DSpace on 2014-12-11T18:23:45Z (GMT). No. of bitstreams: 1 7206950.pdf: 2953370 bytes, checksum: db0d02b43c3dd10cac5a62b060f42dea (MD5) Previous issue date: 1971

    uiuc Repository record

  2. Proving the correctness of program transformations in higher order logic

    Roxas, Rachel Edita Onate1994

    aus-cath Repository record

  3. Proving the correctness of program transformations in higher order logic

    Roxas, Rachel Edita Onate1994

    anu Repository record

  4. Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study

    Martin, Alan J.Université d'Ottawa / University of Ottawa2011

    … and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's …

    ottawa-retro Repository record

  5. A Formal Method to Analyze Framework-Based Software

    Larson, Trent N.2002

    … properties of framework-based software with higher-order logic and then demonstrate its utility for a significant, modern system.

    byu Repository record

  6. Coalgebraic Methods for Object-Oriented Specification

    Tews, HendrikTechnische Universität Dresden

    … a prototype compiler that translates CCSL into higher-order logic.

    qucosa-diss

  7. Stable theories in functional analysis

    Iovino, Jose NicolasUniversity of Illinois at Urbana-Champaign2011

    Model theory is the logical analysis of mathematical structures. The class of structures considered in model theory includes, among others, all structures from algebra, number theory, and finite-dimensional analysis. A limitation, however, is that this class does not include the families of …

    uiuc Repository record

  8. L-Fuzzy Relations in Coq

    Jackson, EthanBrock University2014

    … Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and …

    brock Repository record

  9. Integration of HOL and MDG for hardware verification

    Pisini, Vijay Kumar2000

    … uses the strengths of the theorem prover HOL (Higher-Order Logic) with of the automated tool MDG (Multiway Decision Graphs) which supports equivalence checking and model checking. We developed a linkage tool between HOL and MDG which uses the specification and implementation of a circuit …

    concordia Repository record

  10. Approximation Algorithms using Allegories and Coq

    Chowdhury, DurjayBrock University2017

    … purposes. This language is based on Higher-Order Logic (HOL) with dependent types which support both reasoning and program execution. In addition to the abstract theory, we provide the model of set-theoretic relations between finite sets. This model is executable and used in our …

    brock Repository record

  11. Modular data structure verification

    Kuncak, Viktor (Viktor Jaroslav), 1977-Massachusetts Institute of Technology2007

    … write Jahob specifications in classical higher-order logic (HOL); Jahob reduces the verification problem to deciding the validity of HOL formulas. I present a new method for proving HOL formulas by combining automated reasoning techniques. My method consists of 1) splitting formulas into …

    mit Repository record

  12. Qualitative Spatial Reasoning With Super-Intuitionistic Logics

    Torrini, PaoloUniversity of Leeds2003

    … mereotopology, encodings based on non-classical logics are some of the possible answers that have emerged in connection with this problem. The present analysis is based on the well-known topological semantics of intuitionistic logic. That semantics is considered here from the point of view of the …

    whiterose Repository record

  13. Higher-order proof translation

    Sultana, NikolaiUniversity of Cambridge2015

    The case for interfacing logic tools together has been made countless times in the literature, but it is still an important research question. There are various logics and respective tools for carrying out formal developments, but practitioners still lament the difficulty of reliably exchanging …

    cambridge Repository record

  14. A model checker for statecharts (linking case tools with formal methods)

    Day, Nancy AnnUniversity of British Columbia1993

    … Software Engineering (CASE) tools. In order to create this link, the formalism used by the CASE tool must have a precise formal semantics that can be understood by the verification tool. The CASE tool STATEMATE makes use of an extended state transition notation called statecharts. We …

    ubc Repository record

  15. Optimizing Distributed Transactions: Speculative Client Execution, Certified Serializability, and High Performance Run-Time

    Pandey, UtkarshVirginia Tech2016

    … the same sequence of states by providing a total order to their operations. Thus optimization of both local DBMS operations through concurrency control and the distributed algorithm driving replicated services can lead to enhancing the performance of the on-line services. Deferred Update …

    vt Repository record