Nitpick
From MaRDI portal
Cited in
(only showing first 100 items - show all)- LEO-II
- Nunchaku
- Isabelle/HOL
- RuleML
- AFRA
- THF0
- Tests and proofs for custom data generators
- Darwin
- Instrumenting a weakest precondition calculus for counterexample generation
- Introduction to ``Milestones in interactive theorem proving
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Formally verified algorithms for upper-bounding state space diameters
- A deontic logic reasoning infrastructure
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Validating mathematical theorems and algorithms with RISCAL
- FINDER
- PIDE
- Isabelle/jEdit
- FocalTest
- Satallax
- Sledgehammer
- Kodkod
- Euclide
- QuickCheck
- Quantified multimodal logics in simple type theory
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Alloy*: a general-purpose higher-order relational constraint solver
- FABRIK
- Lem
- EasyCheck
- SmallCheck
- Mechanised assessment of complex natural-language arguments using expressive logic combinations
- HMC
- QMLTP
- KLMLean
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Monotonox
- From LCF to Isabelle/HOL
- Automating free logic in HOL, with an experimental application in category theory
- Blocking and other enhancements for bottom-up model generation methods
- Semantics of Mizar as an Isabelle object logic
- Infinite executions of lazy and strict computations
- On the fine-structure of regular algebra
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
- A decision procedure for (co)datatypes in SMT solvers
- Automating change of representation for proofs in discrete mathematics (extended version)
- MetTeL
- GQML
- Detecting inconsistencies in large first-order knowledge bases
- QuickChick
- AgsyHOL
- LeoPARD
- BVD
- Extensional higher-order paramodulation in Leo-III
- A bi-directional extensible interface between Lean and Mathematica
- Second-order properties of undirected graphs
- On logic embeddings and Gödel's God
- Model finding for recursive functions in SMT
- Effective normalization techniques for HOL
- Tests and Proofs for Enumerative Combinatorics
- HOL Based First-Order Modal Logic Provers
- Verified over-approximation of the diameter of propositionally factored transition systems
- Unifying theories of programming in Isabelle
- MSPASS
- Higher-order modal logics: automation and applications
- A Lambda-Free Higher-Order Recursive Path Order
- An algebraic approach to computations with progress
- Leo-III
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Lem: a lightweight tool for heavyweight semantics
- Automatic proof and disproof in Isabelle/HOL
- RADA
- Alloy*
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- MleanCoP
- FMLtoHOL
- Luck
- DIAMOND
- Automating Change of Representation for Proofs in Discrete Mathematics
- A decision procedure for (co)datatypes in SMT solvers
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Closure, properties and closure properties of multirelations
- Jordan
- RISCAL
- embed_modal
- Jinja Threads
- Myhill-Nerode
- Stern-Brocot Tree
- Markov Models
- Tame Graphs
- Deriving class
- BicolanoMT
- Logic2CNF
- Stone Kleene
- Stone Algebras
- Archive of Formal Proofs
- MadMax
- SMCDEL
- DEMO
- Hotel Key Card
This page was built for software: Nitpick
