China
Africa
Explore chapters and articles related to this topic
Quantum Machine Learning and Big Data for Real-Time Applications
Published in Om Prakash Jena, Sabyasachi Pramanik, Ahmed A. Elngar, Machine Learning Adoption in Blockchain-Based Intelligent Manufacturing, 2022
The first completely validated quantum circuit optimizer (VOQC) was provided by Hietala et al. [19]. In VOQC, Small Quantum Intermediate Representation (SQIR) is a critical component since it provides provable semantics for quantum programs written in the COQ proof assistant. Optimization passes written as COQ functions demonstrate that the semantics of input SQIR programs have been maintained. VOQC’s optimizations are built on the foundation of local circuit equivalences, which are accomplished by substituting one pattern of gates with another or by commuting a gate rightward until it can be canceled [19].
Using the Lean interactive theorem prover in undergraduate mathematics
Published in International Journal of Mathematical Education in Science and Technology, 2023
Interactive theorem provers, also known as computer-based proof assistants, allow users to create and verify mathematical proofs. Several such assistants, notably Coq (https://coq.inria.fr/), Isabelle (https://isabelle.in.tum.de/) and Lean (https://leanprover.github.io), are in current use by practising mathematicians, and have shown their power and usefulness in providing a strong guarantee of correctness (Castelvecchi, 2021; Hanna, Reid, & de Villiers, 2019). As proof assistants become more and more user-friendly, it is not surprising that they are well on the way to being a routine feature of mathematical practice and gaining ground in mathematics teaching. The Lean theorem prover, for example, is propelled by a lively community of users who regularly share their research and teaching experiences, both good and bad, with like-minded colleagues (see Lean’s Zulip channel).
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
Published in Journal of Applied Non-Classical Logics, 2019
Lourdes del Carmen González-Huesca, Favio E. Miranda-Perea, P. Selene Linares-Arévalo
The relevance of modal logic in philosophy and mathematics is well established. Moreover, its importance in computer science has come of age. For instance, the monadic and computational interpretations of modal logic (Bonelli & Feller, 2009; Davies & Pfenning, 2001) for various type theories are deeply related to concurrent and distributed computations (López, Pfenning, Polakow, & Watkins, 2005; Murphy, Crary, Harper, & Pfenning, 2004). These practical applications, originated in different readings of necessity (see Huth & Ryan, 2004, Chapter 5), entail the need for a verification process which nowadays cannot be thought of without the help of an interactive theorem prover. These software programmes, also called proof assistants, are composed of a domain-specific language allowing to represent logical objects, as well as definitions and theorems about them, together with a mechanism that allows for the interactive construction and validation of proofs. The proof development process is driven through a fully interactive goal-oriented proof search, meaning that the search is guided by a human.