Cited in
(only showing first 100 items - show all)- HOL Based First-Order Modal Logic Provers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Tests and Proofs for Enumerative Combinatorics
- Monotonicity inference for higher-order formulas
- Interactive theorem proving from the perspective of Isabelle/Isar
- Monotonicity inference for higher-order formulas
- On logic embeddings and Gödel's God
- A dyadic deontic logic in HOL
- Infinite executions of lazy and strict computations
- A Hierarchy of Algebras for Boolean Subsets
- Quantified multimodal logics in simple type theory
- Automatic proof and disproof in Isabelle/HOL
- Closure, properties and closure properties of multirelations
- On the fine-structure of regular algebra
- LEO-II
- Isabelle/HOL
- RuleML
- AFRA
- THF0
- Darwin
- FINDER
- FocalTest
- Isabelle/jEdit
- PIDE
- Satallax
- Kodkod
- Sledgehammer
- Euclide
- QuickCheck
- FABRIK
- Lem
- EasyCheck
- HMC
- SmallCheck
- KLMLean
- QMLTP
- Monotonox
- GQML
- MetTeL
- AgsyHOL
- QuickChick
- LeoPARD
- BVD
- MSPASS
- Leo-III
- Alloy*
- RADA
- FMLtoHOL
- MleanCoP
- Luck
- DIAMOND
- Jordan
- RISCAL
- embed_modal
- Archive Formal Proofs
- BicolanoMT
- Deriving class
- Jinja Threads
- Markov Models
- Logic2CNF
- Myhill-Nerode
- MadMax
- DEMO
- Hotel Key Card
- SMCDEL
- Stern-Brocot Tree
- Tame Graphs
- Stone Kleene
- Stone Algebras
- CLDC
- LegalRuleML
- Mathematical Components
- Walnut
- AxiomaticCategoryTheory
- GoedelGod
- Kleene Algebra
- Relation Algebra
- Metamath Zero
- Lowe_Ontological_Argument
- PLM
- MetaCoq
- Stone relation algebras
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Beginner's luck: a language for property-based generators
- An algebraic approach to multirelations and their properties
- Higher-order modal logics: automation and applications
- Verifying minimum spanning tree algorithms with Stone relation algebras
- A deontic logic reasoning infrastructure
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- A decision procedure for (co)datatypes in SMT solvers
- Algebras for iteration and infinite computations
- An algebraic approach to computations with progress
- A decision procedure for (co)datatypes in SMT solvers
- Validating mathematical theorems and algorithms with RISCAL
- Evonne
- Formalizing ordinal partition relations using Isabelle/HOL
- Verified over-approximation of the diameter of propositionally factored transition systems
- Semantics of Mizar as an Isabelle object logic
- Computer-supported analysis of arguments in climate engineering
This page was built for software: Nitpick