Nitpick
From MaRDI portal
Software:13377
swMATH622MaRDI QIDQ13377FDOQ13377
Author name not available (Why is that?)
Official website: http://www4.in.tum.de/~blanchet/nitpick.html
Cited In (only showing first 100 items - show all)
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- On the fine-structure of regular algebra
- Verified over-approximation of the diameter of propositionally factored transition systems
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- HOL Based First-Order Modal Logic Provers
- Closure, properties and closure properties of multirelations
- Monotonicity inference for higher-order formulas
- Monotonicity inference for higher-order formulas
- Title not available (Why is that?)
- Verifying minimum spanning tree algorithms with Stone relation algebras
- An algebraic approach to computations with progress
- A deontic logic reasoning infrastructure
- Algebras for iteration and infinite computations
- LEO-II
- AFRA
- 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
- Higher-order modal logics: automation and applications
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Interactive theorem proving from the perspective of Isabelle/Isar
- Quantified multimodal logics in simple type theory
- Beginner's luck: a language for property-based generators
- Metamath Zero
- Lowe_Ontological_Argument
- PLM
- MetaCoq
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- Nunchaku
- Infinite executions of lazy and strict computations
- A Hierarchy of Algebras for Boolean Subsets
- Model finding for recursive functions in SMT
- Automatic proof and disproof in Isabelle/HOL
- An algebraic approach to multirelations and their properties
- Validating mathematical theorems and algorithms with RISCAL
- Tests and Proofs for Enumerative Combinatorics
- On logic embeddings and Gödel's God
- Stone relation algebras
- A dyadic deontic logic in HOL
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Evonne
- Blocking and other enhancements for bottom-up model generation methods
- Formalizing ordinal partition relations using Isabelle/HOL
- A Meta-level Annotation Language for Legal Texts
This page was built for software: Nitpick
