scientific article; zbMATH DE number 234014
From MaRDI portal
Publication:5287513
zbMATH Open0779.68007MaRDI QIDQ5287513FDOQ5287513
Authors:
Publication date: 8 July 1993
Title of this publication is not available (Why is that?)
Recommendations
Cited In (only showing first 100 items - show all)
- From types to sets by local type definition in higher-order logic
- An approach to formal verification of human-computer interaction
- Scalable fine-grained proofs for formula processing
- On the desirability of mechanizing calculational proofs
- Proof assistance for real-time systems using an interactive theorem prover
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
- Adapting functional programs to higher order logic
- Using Structural Recursion for Corecursion
- Formal verification of a programming logic for a distributed programming language
- Title not available (Why is that?)
- Formal analysis of the kinematic Jacobian in screw theory
- Mechanized metatheory revisited
- The proof monad
- Simplifying proofs in Fitch-style natural deduction systems
- Programmed strategies for program verification
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- A theory of formal synthesis via inductive learning
- A formal proof of the Kepler conjecture
- A proof-centric approach to mathematical assistants
- Formalization of the standard uniform random variable
- An exercise in the automatic verification of asynchronous designs
- Providing a formal linkage between MDG and HOL
- A few exercises in theorem processing
- Title not available (Why is that?)
- Lazy techniques for fully expansive theorem proving
- The \(HOL\) logic extended with quantification over type variables
- Implementing geometric algebra products with binary trees
- Soundness and completeness proofs by coinductive methods
- Hybrid interactive theorem proving using Nuprl and HOL
- A complete axiom system for propositional projection temporal logic with cylinder computation model
- Without Loss of Generality
- Formal probabilistic analysis of detection properties in wireless sensor networks
- Using theorem proving to verify expectation and variance for discrete random variables
- Proof assistants: history, ideas and future
- Algebraic models of correctness for abstract pipelines.
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Formalization of entropy measures in HOL
- A mechanical analysis of program verification strategies
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formalization of the C99 standard in HOL, Isabelle and Coq
- Unifying theories in ProofPower-Z
- The calculus of constructions as a framework for proof search with set variable instantiation
- Logic-based subsumption architecture
- A complete mechanization of correctness of a string-preprocessing algorithm
- Formalization of fixed-point arithmetic in HOL
- Deductive verification of real-time systems using STeP
- A consistent foundation for Isabelle/HOL
- A consistent foundation for Isabelle/HOL
- Proof search with set variable instantiation in the calculus of constructions
- Extended Static Checking by Calculation Using the Pointfree Transform
- Formal Analysis of Optical Waveguides in HOL
- A scalable module system
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Semantic essence of AsmL
- Unifying sets and programs via dependent types
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Formal reliability analysis of combinational circuits using theorem proving
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Theories for mechanical proofs of imperative programs
- The seven virtues of simple type theory
- The HOL-Omega Logic
- A decision procedure for linear ``big O equations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program derivation with verified transformations — a case study
- Combining Decision Procedures by (Model-)Equality Propagation
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A Brief Overview of HOL4
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- Higher-order rewrite systems and their confluence
- Higher-order semantics and extensionality
- A framework for the verification of certifying computations
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Combining decision procedures by (model-)equality propagation
- Mechanised wire-wise verification of Handel-C synthesis
- Monotonicity inference for higher-order formulas
- Analytic tableaux for higher-order logic with choice
- Monotonicity inference for higher-order formulas
- Local Theory Specifications in Isabelle/Isar
- Isabelle/HOL. A proof assistant for higher-order logic
- Computer supported mathematics with \(\Omega\)MEGA
- Compressing propositional refutations
- Proof synthesis and reflection for linear arithmetic
- Efficiently checking propositional refutations in HOL theorem provers
- Integrating external deduction tools with ACL2
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- N. G. de Bruijn's contribution to the formalization of mathematics
- Formal analysis of optical systems
- PVS embedding of cCSP semantic models and their relationship
- Optimizing proof search in model elimination
- A linear logical framework
- A rewriting approach to satisfiability procedures.
- ML
- Evaluating general purpose automated theorem proving systems
- Automatic verification of reduction techniques in higher order logic
- On Correctness of Mathematical Texts from a Logical and Practical Point of View
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5287513)
