scientific article
From MaRDI portal
Publication:2729065
zbMath0971.68627MaRDI QIDQ2729065
Publication date: 6 November 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) ⋮ Supporting the formal verification of mathematical texts ⋮ Hammer for Coq: automation for dependent type theory ⋮ Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface ⋮ Tactics for hierarchical proof ⋮ Automation for interactive proof: first prototype ⋮ The Isabelle Framework ⋮ Recycling proof patterns in Coq: case studies ⋮ User interaction with the Matita proof assistant ⋮ Managing Proof Documents for Asynchronous Processing ⋮ A User Interface for a Mathematical System that Allows Ambiguous Formulae ⋮ Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ From LCF to Isabelle/HOL ⋮ The Matita Interactive Theorem Prover ⋮ Isabelle as Document-Oriented Proof Assistant ⋮ Proof General ⋮ Formal Proof: Reconciling Correctness and Understanding ⋮ Interactive Simplifier Tracing and Debugging in Isabelle ⋮ Enhancing Theorem Prover Interfaces with Program Slice Information ⋮ Web Interfaces for Proof Assistants ⋮ Tinycals: Step by Step Tacticals
Uses Software
