An Automated Deductive Verification Framework for Circuit-building Quantum Programs

AbstractWhile recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.

Download Full-text

A universal inductive inference machine

Journal of Symbolic Logic ◽

10.2307/2274708 ◽

1991 ◽

Vol 56 (2) ◽

pp. 661-672 ◽

Cited By ~ 21

Author(s):

Daniel N. Osherson ◽

Michael Stob ◽

Scott Weinstein

Keyword(s):

Inductive Inference ◽

Scientific Discovery ◽

Order Logic ◽

First Order Logic ◽

Logical Framework ◽

First Order

AbstractA paradigm of scientific discovery is defined within a first-order logical framework. It is shown that within this paradigm there exists a formal scientist that is Turing computable and universal in the sense that it solves every problem that any scientist can solve. It is also shown that universal scientists exist for no regular logics that extend first-order logic and satisfy the Löwenheim-Skolem condition.

Download Full-text

Formalization Of Theories of Design Using: First Order Logic Augmented With A Causal Calculus; And Entropy of a Design Defined In Terms Of The Function, Behavior and Structure Ontology.

10.31224/osf.io/2m763 ◽

2021 ◽

Author(s):

KARTHIK GURUMURTHI

Keyword(s):

High Probability ◽

Formal Proof ◽

Order Logic ◽

First Order Logic ◽

Logical Framework ◽

Seamless Integration ◽

Good Design ◽

First Order ◽

Individual Variables ◽

And Behavior

A symbolic logical framework (L) consisting of first order logic augmented with a causal calculus has been provided to formalize, axiomatize and integrate theories of design. L is used to represent designs in the Function-Behavior-Structure (FBS) ontology in a single, widely applicable language that enables the following: seamless integration of representations of function, behavior and structure; and generality in the formalization of theories of design. FRs, constraints, structure and behavior are represented as sentences in L. FRs are represented (as abstractions of behavior) in the form of existentially quantified sentences, the instantiation of whose individual variables yields the representation of behavior. This enables the logical implication of FRs by behavior, without recourse to apriori criteria for satisfaction of FRs by behavior. Functional decomposition is represented to enable lower level FRs to logically imply the satisfaction of higher level FRs. The theory of whether and how structure and behavior satisfy FRs and constraints is represented as a formal proof in L. Important general attributes of designs such as solution-neutrality of FRs, probability of satisfaction of requirements and constraints (calculated in a Bayesian framework using Monte Carlo simulation), extent and nature of coupling, etc. have been defined in terms of the representation of a design in L. The entropy of a design is defined in terms of the above attributes of a design, based on which a general theory of what constitutes a good design has been formalized to include the desirability of solution-neutrality of (especially higher level) FRs, high probability of satisfaction of requirements and constraints, wide specifications, low variability and bias, use of fewer attributes to specify the design, less coupling (especially circular coupling at higher levels of FRs), parametrization, standardization, etc..

Download Full-text

Connecting a Logical Framework to a First-Order Logic Prover

Frontiers of Combining Systems - Lecture Notes in Computer Science ◽

10.1007/11559306_17 ◽

2005 ◽

pp. 285-301 ◽

Cited By ~ 8

Author(s):

Andreas Abel ◽

Thierry Coquand ◽

Ulf Norell

Keyword(s):

Order Logic ◽

First Order Logic ◽

Logical Framework ◽

First Order

Download Full-text

Modular specification and verification of closures in Rust

Proceedings of the ACM on Programming Languages ◽

10.1145/3485522 ◽

2021 ◽

Vol 5 (OOPSLA) ◽

pp. 1-29

Author(s):

Fabian Wolff ◽

Aurel Bílý ◽

Christoph Matheja ◽

Peter Müller ◽

Alexander J. Summers

Keyword(s):

Formal Verification ◽

Functional Properties ◽

Type System ◽

Order Logic ◽

First Order Logic ◽

Formal Reasoning ◽

First Order ◽

Novel Technique ◽

Smt Solvers ◽

Specification And Verification

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.

Download Full-text

“Most of” leads to undecidability: Failure of adding frequencies to LTL

Lecture Notes in Computer Science - Foundations of Software Science and Computation Structures ◽

10.1007/978-3-030-71995-1_5 ◽

2021 ◽

pp. 82-101

Author(s):

Bartosz Bednarczyk ◽

Jakub Michaliszyn

Keyword(s):

Model Checking ◽

Formal Verification ◽

Temporal Logic ◽

Order Logic ◽

First Order Logic ◽

Statistical Reasoning ◽

First Order ◽

High Interest ◽

The Past ◽

Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

Download Full-text

SKEPTICAL ABDUCTION

International Journal of Artificial Intelligence Tools ◽

10.1142/s0218213093000242 ◽

1993 ◽

Vol 02 (04) ◽

pp. 511-540 ◽

Cited By ~ 2

Author(s):

P. MARQUIS

Keyword(s):

Propositional Logic ◽

Order Logic ◽

First Order Logic ◽

Real Problem ◽

Logical Framework ◽

First Order ◽

Selective Generation ◽

The Given ◽

Reasonable Prospect

Abduction is the process of generating the best explanation as to why a fact is observed given what is already known. A real problem in this area is the selective generation of hypotheses that have some reasonable prospect of being valid. In this paper, we propose the notion of skeptical abduction as a model to face this problem. Intuitively, the hypotheses pointed out by skeptical abduction are all the explanations that are consistent with the given knowledge and that are minimal, i.e. not unnecessarily general. Our contribution is twofold. First, we present a formal characterization of skeptical abduction in a logical framework. On this ground, we address the problem of mechanizing skeptical abduction. A new method to compute minimal and consistent hypotheses in propositional logic is put forward. The extent to which skeptical abduction can be mechanized in first—order logic is also investigated. In particular, two classes of first-order formulas in which skeptical abduction is effective are provided. As an illustration, we finally sketch how our notion of skeptical abduction applies as a theoretical tool to some artificial intelligence problems (e.g. diagnosis, machine learning).

Download Full-text

An Overview of VV&A Methods for Conceptual Model

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.444-445.860 ◽

2013 ◽

Vol 444-445 ◽

pp. 860-864

Author(s):

Xiao Jian Ding ◽

Feng Xin Sun

Keyword(s):

Petri Nets ◽

Formal Verification ◽

Conceptual Model ◽

Conceptual Modeling ◽

Order Logic ◽

Model Verification ◽

First Order Logic ◽

Verification Method ◽

First Order ◽

Formal Techniques

This paper summarizes the literature and presents important concepts related to conceptual model verification. Different approaches have been proposed in the literature. These approaches have been introduced as two parts with emphasis on formal techniques. First order logic for structural views and Petri nets for behavioral views are investigated in the search of a practical verification method for conceptual modeling in UML. Then a short assessment of formal verification work for UML will be presented.

Download Full-text

Equivalences between logics and their representing type theories

Mathematical Structures in Computer Science ◽

10.1017/s0960129500000785 ◽

1995 ◽

Vol 5 (3) ◽

pp. 323-349 ◽

Cited By ~ 1

Author(s):

Philippa Gardner

Keyword(s):

Natural Deduction ◽

Order Logic ◽

First Order Logic ◽

Logical Framework ◽

Simple Formulation ◽

First Order ◽

Relevant Logics ◽

First Time ◽

New Framework

We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF+, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.

Download Full-text