Isabelle/HOL

No author found.

Related Items (only showing first 100 items - show all)

Theorem proving graph grammars with attributes and negative application conditions ⋮ Using relation-algebraic means and tool support for investigating and computing bipartitions ⋮ Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A decision procedure for (co)datatypes in SMT solvers ⋮ Proving divide and conquer complexities in Isabelle/HOL ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Soundness and completeness proofs by coinductive methods ⋮ Variants of Gödel's ontological proof in a natural deduction calculus ⋮ From LTL to deterministic automata. A safraless compositional approach ⋮ A verified algorithm enumerating event structures ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings ⋮ The gauge integral theory in HOL4 ⋮ A unified framework for DPLL(T) + certificates ⋮ From informal to formal proofs in Euclidean geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Invariants for the FoCaL language ⋮ Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings ⋮ A decision procedure for linear ``big O equations ⋮ Verification of clock synchronization algorithms: experiments on a combination of deductive tools ⋮ Code-carrying theories ⋮ Semantics, calculi, and analysis for object-oriented specifications ⋮ Proof Pearl: regular expression equivalence and relation algebra ⋮ A canonical locally named representation of binding ⋮ Formalizing adequacy: a case study for higher-order abstract syntax ⋮ A two-level logic approach to reasoning about computations ⋮ Social choice theory in HOL. Arrow and Gibbard-Satterthwaite ⋮ Predictive runtime enforcement ⋮ Efficient certified RAT verification ⋮ Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems ⋮ Certifying safety and termination proofs for integer transition systems ⋮ A proof strategy language and proof script generation for Isabelle/HOL ⋮ A formal, resource consumption-preserving translation of actors to Haskell ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ A corrected quantitative version of the Morse lemma ⋮ Finite integer computations: An algebraic foundation for their correctness ⋮ Automation for interactive proof: first prototype ⋮ A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation ⋮ Why do the relativistic masses and momenta of faster-than-light particles decrease as their speeds increase? ⋮ Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates ⋮ Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book ⋮ A program logic for resources ⋮ Translating higher-order clauses to first-order clauses ⋮ Proving pointer programs in higher-order logic ⋮ An algebra of synchronous atomic steps ⋮ Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings ⋮ Mechanically proving determinacy of hierarchical block diagram translations ⋮ Interaction with formal mathematical documents in Isabelle/PIDE ⋮ Beginners' quest to formalize mathematics: a feasibility study in Isabelle ⋮ A tale of two set theories ⋮ Lemma discovery for induction. A survey ⋮ Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL ⋮ The Coq library as a theory graph ⋮ Inspection and selection of representations ⋮ Formalization of function matrix theory in HOL ⋮ Solution methods for a min-max facility location problem with regional customers considering closest Euclidean distances ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Priority inheritance protocol proved correct ⋮ Solving quantifier-free first-order constraints over finite sets and binary relations ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Extending SMT solvers to higher-order logic ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ GRUNGE: a grand unified ATP challenge ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Certified equational reasoning via ordered completion ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Mechanized metatheory revisited ⋮ Classification of finite fields with applications ⋮ An Isabelle/HOL formalisation of Green's theorem ⋮ A verified compiler from Isabelle/HOL to CakeML ⋮ Hierarchical specification and verification of architectural design patterns ⋮ Efficient verification of imperative programs using auto2 ⋮ Hoare logics for time bounds. A study in meta theory ⋮ Model-theoretic conservative extension for definitional theories ⋮ Non-standard analysis in dynamic geometry ⋮ Interactive verification of architectural design patterns in FACTum ⋮ Term-generic logic ⋮ Infinite executions of lazy and strict computations ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ Modelling algebraic structures and morphisms in ACL2 ⋮ A framework for the verification of certifying computations ⋮ Using Isabelle/HOL to verify first-order relativity theory ⋮ Reducing higher-order theorem proving to a sequence of SAT problems ⋮ Extending Sledgehammer with SMT solvers ⋮ Proof pearl: A mechanized proof of GHC's mergesort ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ Formalization of Shannon's theorems ⋮ On the formalization of gamma function in HOL ⋮ On the fine-structure of regular algebra ⋮ Formalizing complex plane geometry ⋮ Formalizing provable anonymity in Isabelle/HOL

This page was built for software: Isabelle/HOL