Cited in
(only showing first 100 items - show all)- A dyadic deontic logic in HOL
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Blocking and other enhancements for bottom-up model generation methods
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- On the fine-structure of regular algebra
- ProofWidgets
- Verified over-approximation of the diameter of propositionally factored transition systems
- Formalizing ordinal partition relations using Isabelle/HOL
- A Meta-level Annotation Language for Legal Texts
- Towards an Executable Methodology for the Formalization of Legal Texts
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- scientific article; zbMATH DE number 7633799 (Why is no real title available?)
- HOL Based First-Order Modal Logic Provers
- Extensional higher-order paramodulation in Leo-III
- Tests and proofs for custom data generators
- Automating Change of Representation for Proofs in Discrete Mathematics
- Closure, properties and closure properties of multirelations
- Alloy*: a general-purpose higher-order relational constraint solver
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Generating counterexamples for structural inductions by exploiting nonstandard models
- Monotonicity inference for higher-order formulas
- An algebraic approach to computations with progress
- Computer-supported analysis of arguments in climate engineering
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Monotonicity inference for higher-order formulas
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- A deontic logic reasoning infrastructure
- Algebras for iteration and infinite computations
- Effective normalization techniques for HOL
- Automating change of representation for proofs in discrete mathematics (extended version)
- Instrumenting a weakest precondition calculus for counterexample generation
- 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
This page was built for software: Nitpick
