The Experts below are selected from a list of 84 Experts worldwide ranked by ideXlab platform

J. W. Sanders - One of the best experts on this subject based on the ideXlab platform.

  • Idempotent Relations in Isabelle/HOL
    Lecture Notes in Computer Science, 2005
    Co-Authors: Florian Kammüller, J. W. Sanders
    Abstract:

    A characterization of idempotent relations is presented first as a paper-style proof, then by its formalization in Isabelle/HOL. The novel characterization gives rise to the construction of idempotent relations by an abstract algorithm. This algorithm is rigorously developed inside Isabelle/HOL using Primitive Recursive Function definitions. Whilst the characterisation and algorithm appear to be new, we regard this as an interesting demonstration of the interplay between mathematical reasoning and program development, in particular using Isabelle/HOL.

  • ICTAC - Idempotent relations in Isabelle/HOL
    Theoretical Aspects of Computing - ICTAC 2004, 2005
    Co-Authors: Florian Kammüller, J. W. Sanders
    Abstract:

    A characterization of idempotent relations is presented first as a paper-style proof, then by its formalization in Isabelle/HOL. The novel characterization gives rise to the construction of idempotent relations by an abstract algorithm. This algorithm is rigorously developed inside Isabelle/HOL using Primitive Recursive Function definitions. Whilst the characterisation and algorithm appear to be new, we regard this as an interesting demonstration of the interplay between mathematical reasoning and program development, in particular using Isabelle/HOL.

Florian Kammüller - One of the best experts on this subject based on the ideXlab platform.

  • Idempotent Relations in Isabelle/HOL
    Lecture Notes in Computer Science, 2005
    Co-Authors: Florian Kammüller, J. W. Sanders
    Abstract:

    A characterization of idempotent relations is presented first as a paper-style proof, then by its formalization in Isabelle/HOL. The novel characterization gives rise to the construction of idempotent relations by an abstract algorithm. This algorithm is rigorously developed inside Isabelle/HOL using Primitive Recursive Function definitions. Whilst the characterisation and algorithm appear to be new, we regard this as an interesting demonstration of the interplay between mathematical reasoning and program development, in particular using Isabelle/HOL.

  • ICTAC - Idempotent relations in Isabelle/HOL
    Theoretical Aspects of Computing - ICTAC 2004, 2005
    Co-Authors: Florian Kammüller, J. W. Sanders
    Abstract:

    A characterization of idempotent relations is presented first as a paper-style proof, then by its formalization in Isabelle/HOL. The novel characterization gives rise to the construction of idempotent relations by an abstract algorithm. This algorithm is rigorously developed inside Isabelle/HOL using Primitive Recursive Function definitions. Whilst the characterisation and algorithm appear to be new, we regard this as an interesting demonstration of the interplay between mathematical reasoning and program development, in particular using Isabelle/HOL.

E. V. Krishnamurthy - One of the best experts on this subject based on the ideXlab platform.

  • International Conference on Computational Science - Problems and prospects for quantum computational speed-up
    Lecture Notes in Computer Science, 2003
    Co-Authors: E. V. Krishnamurthy
    Abstract:

    This paper studies the problems involved in the speed-up of the classical computational algorithms using the quantum computational paradigm. In particular, we relate the Primitive Recursive Function approach used in computability theory with the harmonic oscillator basis used in quantum physics. Also, we raise some basic issues concerning quantum computational paradigm: these include failures in programmability and scalability, limitation on the size of the decoherence - free space available and lack of methods for proving quantum programs correct. In computer science, time is discrete and has a well-founded structure. But in physics, time is a real number, continuous and is infinitely divisible; also time can have a fractal dimension. As a result, the time complexity measures for conventional and quantum computation are incomparable. Proving properties of programs and termination rest heavily on the well-founded properties, and the transfinite induction principle. Hence transfinite induction is not applicable to reason about quantum programs.

Sten Agerholm - One of the best experts on this subject based on the ideXlab platform.

  • Non-Primitive Recursive Function Definitions
    BRICS Report Series, 1995
    Co-Authors: Sten Agerholm
    Abstract:

    This paper presents an approach to the problem of introducing non-Primitive Recursive Function definitions in higher order logic. A Recursive specification is translated into a domain theory version, where the Recursive calls are treated as potentially non-terminating. Once we have proved termination, the original specification can be derived easily. A collection of algorithms are presented which hide the domain theory from a user. Hence, the derivation of a domain theory specification has been automated completely, and for well-founded Recursive Function specifications the process of deriving the original specification from the domain theory one has been automated as well, though a user must supply a well-founded relation and prove certain termination properties of the specification. There are constructions for building well-founded relations easily.

  • TPHOLs - Non-Primitive Recursive Function Definitions
    Higher Order Logic Theorem Proving and Its Applications, 1995
    Co-Authors: Sten Agerholm
    Abstract:

    This paper presents an approach to the problem of introducing non-Primitive Recursive Function definitions in higher order logic. A Recursive specification is translated into a domain theory version, where the Recursive calls are treated as potentially non-terminating. Once we have proved termination, the original specification can be derived easily. A collection of algorithms are presented which hide the domain theory from a user. Hence, the derivation of a domain theory specification has been automated completely, and for well-founded Recursive Function specifications the process of deriving the original specification from the domain theory one has been automated as well, though a user must supply a well-founded relation and prove certain termination properties of the specification. There are constructions for building well-founded relations easily.

Andrea Sattler-klein - One of the best experts on this subject based on the ideXlab platform.

  • LPAR - Infinite, Canonical String Rewriting Systems Generated by Completion
    Logic Programming and Automated Reasoning, 1
    Co-Authors: Andrea Sattler-klein
    Abstract:

    Most versions of the Knuth-Bendix completion ’procedure’ are designed to compute when possible a canonical rewriting system. We show that even for string rewriting systems (SRSs) canonical systems may be generated by completion which are not Recursively enumerable. This may happen also if the SRS has decidable word problem. We analyze how this phenomenon depends on the ordering used for completion. It turns out that in general if a SRS is completed with respect to a length-lexicographic ordering divergence sequences encoding the input/output behaviour of any Primitive Recursive Function as well as any Recursively enumerable set and some non Recursively enumerable sets may be generated. But, if a SRS with decidable word problem is completed with such an ordering, then the generated canonical system will be Recursive.