scientific article; zbMATH DE number 234014
From MaRDI portal
Publication:5287513
zbMath0779.68007MaRDI QIDQ5287513
No author found.
Publication date: 8 July 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
An exercise in the automatic verification of asynchronous designs, Soundness and completeness proofs by coinductive methods, Theory morphisms in Church's type theory with quotation and evaluation, Weakest pre-condition reasoning for Java programs with JML annotations, Formal analysis of the kinematic Jacobian in screw theory, The higher-order prover \textsc{Leo}-II, Semi-intelligible Isar proofs from machine-generated proofs, Interpreting HOL in the calculus of constructions, Secure mechanical verification of mutually recursive procedures, Proof pearl: Mechanizing the textbook proof of Huffman's algorithm, The role of entropy in guiding a connection prover, Simplifying proofs in Fitch-style natural deduction systems, Ordinal arithmetic: Algorithms and mechanization, Joshua Guttman: pioneering strand spaces, Deciding Boolean algebra with Presburger arithmetic, Program logic for higher-order probabilistic programs in Isabelle/HOL, An approach to literate and structured formal developments, TPS: A hybrid automatic-interactive system for developing proofs, A proof-centric approach to mathematical assistants, Computer supported mathematics with \(\Omega\)MEGA, SAD as a mathematical assistant -- how should we go from here to there?, A two-valued logic for properties of strict functional programs allowing partial functions, CryptHOL: game-based proofs in higher-order logic, Providing a formal linkage between MDG and HOL, A few exercises in theorem processing, A theory of formal synthesis via inductive learning, TPS: A theorem-proving system for classical type theory, Higher-order rewrite systems and their confluence, An approach for lifetime reliability analysis using theorem proving, A mechanisation of some context-free language theory in HOL4, A scalable module system, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Unifying sets and programs via dependent types, A complete axiom system for propositional projection temporal logic with cylinder computation model, A linear logical framework, Verifying a scheduling protocol of safety-critical systems, A rewriting approach to satisfiability procedures., Unifying theories in ProofPower-Z, Formal probabilistic analysis of detection properties in wireless sensor networks, Automation for interactive proof: first prototype, Formal reasoning about finite-state discrete-time Markov chains in HOL, Mechanised wire-wise verification of Handel-C synthesis, Combining decision procedures by (model-)equality propagation, Monotonicity inference for higher-order formulas, Analytic tableaux for higher-order logic with choice, Unique solutions of contractions, CCS, and their HOL formalisation, Algebraic models of correctness for abstract pipelines., From types to sets by local type definition in higher-order logic, Automatic verification of reduction techniques in higher order logic, A mechanical analysis of program verification strategies, Formal analysis of optical systems, A consistent foundation for Isabelle/HOL, Term rewriting and Hoare logic -- Coded rewriting, Proof synthesis and reflection for linear arithmetic, The seven virtues of simple type theory, Incorporating quotation and evaluation into Church's type theory, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4, Reasoning about conditional probabilities in a higher-order-logic theorem prover, Formal reliability analysis of combinational circuits using theorem proving, Partial and nested recursive function definitions in higher-order logic, The proof monad, Organizing numerical theories using axiomatic type classes, From LCF to Isabelle/HOL, Milestones from the Pure Lisp Theorem Prover to ACL2, Formalization of the standard uniform random variable, A UTP semantics for communicating processes with shared variables and its formal encoding in PVS, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Integrating external deduction tools with ACL2, Efficiently checking propositional refutations in HOL theorem provers, N. G. de Bruijn's contribution to the formalization of mathematics, Implementing geometric algebra products with binary trees, Limited second-order functionality in a first-order setting, ML, Superposition for full higher-order logic, Theories for mechanical proofs of imperative programs, GRUNGE: a grand unified ATP challenge, Adapting functional programs to higher order logic, Formal verification of a programming logic for a distributed programming language, Mechanized metatheory revisited, Formalization of geometric algebra in HOL Light, Proof assistants: history, ideas and future, The calculus of constructions as a framework for proof search with set variable instantiation, Data compression for proof replay, Using theorem proving to verify expectation and variance for discrete random variables, Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation, Deductive verification of real-time systems using STeP, Structuring metatheory on inductive definitions, The \(HOL\) logic extended with quantification over type variables, Lazy techniques for fully expansive theorem proving, Proof assistance for real-time systems using an interactive theorem prover, A framework for the verification of certifying computations, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Evaluating general purpose automated theorem proving systems, On the formalization of gamma function in HOL, On the desirability of mechanizing calculational proofs, Logic-based subsumption architecture, A complete mechanization of correctness of a string-preprocessing algorithm, Two case studies of semantics execution in Maude: CCS and LOTOS, Formalization of fixed-point arithmetic in HOL, A FORMAL PROOF OF THE KEPLER CONJECTURE, The Imandra Automated Reasoning System (System Description), Automatic Proof and Disproof in Isabelle/HOL, Combining Model Checking and Deduction, Symbolic Trajectory Evaluation, A restricted form of higher-order rewriting applied to an HDL semantics, Without Loss of Generality, HOL Light: An Overview, Formal Analysis of Optical Waveguides in HOL, The HOL-Omega Logic, A compiled implementation of normalisation by evaluation, A decision procedure for linear ``big O equations, Mechanizing common knowledge logic using COQ, More Church-Rosser proofs (in Isabelle/HOL), Higher-order semantics and extensionality, Computational logic: its origins and applications, Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology, Structuring metatheory on inductive definitions, Computer assisted reasoning. A Festschrift for Michael J. C. Gordon, Formalizing an analytic proof of the prime number theorem, Rewriting conversions implemented with continuations, Characteristics of de Bruijn’s early proof checker Automath, Auto in Agda, Extensional higher-order paramodulation in Leo-III, A Consistent Foundation for Isabelle/HOL, Unnamed Item, A formalised theorem in the partition calculus, A realizability interpretation of Church's simple theory of types, Assumption-based runtime verification, Solving modal logic problems by translation to higher-order logic, Superposition for higher-order logic, Combining higher-order logic with set theory formalizations, Hoare logic for Java in Isabelle/HOL, Automated reasoning for probabilistic sequential programs with theorem proving, Program derivation with verified transformations — a case study, Friends with Benefits, Comprehending Isabelle/HOL’s Consistency, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), THF0 – The Core of the TPTP Language for Higher-Order Logic, Unnamed Item, A Brief Overview of HOL4, A Compiled Implementation of Normalization by Evaluation, LCF-Style Propositional Simplification with BDDs and SAT Solvers, Proof Pearl: Revisiting the Mini-rubik in Coq, Dealing with algebraic expressions over a field in Coq using Maple, An approach to formal verification of human-computer interaction, Machine-Checked Proof-Theory for Propositional Modal Logics, Fixpoints and Search in PVS, R n - and G n -logics, Abstraction of hardware construction, An embedding of Ruby in Isabelle, Mechanical verification of mutually recursive procedures, Optimizing proof search in model elimination, Reflection of formal tactics in a deductive reflection framework, Proof search with set variable instantiation in the Calculus of Constructions, Circuits as streams in Coq: Verification of a sequential multiplier, Reflection principles for synthetic theories of smooth manifolds, Translating higher-order clauses to first-order clauses, The Strategy Challenge in SMT Solving, Error analysis of digital filters using HOL theorem proving, Efficient Substitution in Hoare Logic Expressions, Partiality and recursion in interactive theorem provers – an overview, A higher-order interpretation of deductive tableau, PVS Embedding of cCSP Semantic Models and Their Relationship, Compressing Propositional Refutations, Combining Decision Procedures by (Model-)Equality Propagation, Analytic Tableaux for Higher-Order Logic with Choice, Monotonicity Inference for Higher-Order Formulas, Extended Static Checking by Calculation Using the Pointfree Transform, An untyped higher order logic with Y combinator, Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays, Unifying Sets and Programs via Dependent Types, Formal verification of tail distribution bounds in the HOL theorem prover, A Formalization of the C99 Standard in HOL, Isabelle and Coq, Formalizing Bachmair and Ganzinger's ordered resolution prover, Verifying safety critical task scheduling systems in PPTL axiom system, Superposition with lambdas, Scalable fine-grained proofs for formula processing, Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics, Formalization of Entropy Measures in HOL, Local Theory Specifications in Isabelle/Isar, Using Structural Recursion for Corecursion, HOL Zero’s Solutions for Pollack-Inconsistency, From Types to Sets by Local Type Definitions in Higher-Order Logic, LCF-style Platform based on Multiway Decision Graphs, Hybrid interactive theorem proving using nuprl and HOL, On Correctness of Mathematical Texts from a Logical and Practical Point of View, Semantic essence of AsmL, Probabilistic guarded commands mechanized in HOL, Programmed Strategies for Program Verification, Mechanizing Nonstandard Real Analysis, A Logical Framework with Explicit Conversions
Uses Software
