Nitpick
From MaRDI portal
Software:13377
swMATH622MaRDI QIDQ13377FDOQ13377
Author name not available (Why is that?)
Cited In (72)
- A Meta-level Annotation Language for Legal Texts
- Computer-Supported Exploration of a Categorical Axiomatization of Modeloids
- Towards an Executable Methodology for the Formalization of Legal Texts
- Title not available (Why is that?)
- Lem: A Lightweight Tool for Heavyweight Semantics
- Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- A Nitpick analysis of Mobile IPv6
- Title not available (Why is that?)
- Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
- Title not available (Why is that?)
- Constraint solving for finite model finding in SMT solvers
- 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
- Blocking and other enhancements for bottom-up model generation methods
- On the fine-structure of regular algebra
- Model Finding for Recursive Functions in SMT
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- HOL Based First-Order Modal Logic Provers
- Automating Change of Representation for Proofs in Discrete Mathematics
- Extensional higher-order paramodulation in Leo-III
- Automatic Proof and Disproof in Isabelle/HOL
- Tests and proofs for custom data generators
- Alloy*: a general-purpose higher-order relational constraint solver
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
- Monotonicity Inference for Higher-Order Formulas
- A deontic logic reasoning infrastructure
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
- Algebras for iteration and infinite computations
- Automating change of representation for proofs in discrete mathematics (extended version)
- Instrumenting a weakest precondition calculus for counterexample generation
- Introduction to ``Milestones in interactive theorem proving
- Formally verified algorithms for upper-bounding state space diameters
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Closure, Properties and Closure Properties of Multirelations
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
- Title not available (Why is that?)
- Stone Relation Algebras
- Quantified multimodal logics in simple type theory
- αCheck: A mechanized metatheory model checker
- Beginner's luck: a language for property-based generators
- Effective Normalization Techniques for HOL
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- A bi-directional extensible interface between Lean and Mathematica
- From LCF to Isabelle/HOL
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- Mechanised assessment of complex natural-language arguments using expressive logic combinations
- Computational logic: its origins and applications
- A decision procedure for (co)datatypes in SMT solvers
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Infinite executions of lazy and strict computations
- A Hierarchy of Algebras for Boolean Subsets
- Semantics of Mizar as an Isabelle object logic
- A Lambda-Free Higher-Order Recursive Path Order
- Automating free logic in HOL, with an experimental application in category theory
- The New Quickcheck for Isabelle
- On Logic Embeddings and Gödel’s God
- Second-order properties of undirected graphs
- Higher-Order Modal Logics: Automation and Applications
- Computer-Supported Analysis of Arguments in Climate Engineering
- Unifying Theories of Programming in Isabelle
- An algebraic approach to multirelations and their properties
- Validating mathematical theorems and algorithms with RISCAL
- Detecting inconsistencies in large first-order knowledge bases
- Tests and Proofs for Enumerative Combinatorics
- A Decision Procedure for (Co)datatypes in SMT Solvers
This page was built for software: Nitpick