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)
- 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
- Analytic tableaux for higher-order logic with choice
- Partiality and recursion in interactive theorem provers -- an overview
- Deciding Boolean algebra with Presburger arithmetic
- TPS: A theorem-proving system for classical type theory
- A compiled implementation of normalisation by evaluation
- Weakest pre-condition reasoning for Java programs with JML annotations
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- A two-valued logic for properties of strict functional programs allowing partial functions
- TPS: A hybrid automatic-interactive system for developing proofs
- SAD as a mathematical assistant -- how should we go from here to there?
- Data compression for proof replay
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- On the formalization of gamma function in HOL
- Ordinal arithmetic: Algorithms and mechanization
- Hoare logic for Java in Isabelle/HOL
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A Compiled Implementation of Normalization by Evaluation
- Translating higher-order clauses to first-order clauses
- Formal verification of tail distribution bounds in the HOL theorem prover
- Partial and nested recursive function definitions in higher-order logic
- Probabilistic guarded commands mechanized in HOL
- Secure mechanical verification of mutually recursive procedures
- Fixpoints and search in PVS
- Automatic proof and disproof in Isabelle/HOL
- HOL Light: An Overview
- Automation for interactive proof: first prototype
- Friends with benefits. Implementing corecursion in foundational proof assistants
- A mechanisation of some context-free language theory in HOL4
- An approach for lifetime reliability analysis using theorem proving
- Term rewriting and Hoare logic -- Coded rewriting
- 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
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)
