Nitpick

swMATH622MaRDI QIDQ13377FDOQ13377

Author name not available (Why is that?)

Described by source

• Nitpick: a counterexample generator for higher-order logic based on a relational model finder

Cited In (72)

• A Meta-level Annotation Language for Legal Texts
• Towards an Executable Methodology for the Formalization of Legal Texts
• Title not available (Why is that?)
• Generating counterexamples for structural inductions by exploiting nonstandard models
• Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
• Computer-supported exploration of a categorical axiomatization of modeloids
• Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
• A Nitpick analysis of Mobile IPv6
• Title not available (Why is that?)
• Lem: a lightweight tool for heavyweight semantics
• 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
• Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
• On the fine-structure of regular algebra
• Formalizing ordinal partition relations using Isabelle/HOL
• 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
• Automating Change of Representation for Proofs in Discrete Mathematics
• Extensional higher-order paramodulation in Leo-III
• Closure, properties and closure properties of multirelations
• Tests and proofs for custom data generators
• Alloy*: a general-purpose higher-order relational constraint solver
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Computer-supported analysis of arguments in climate engineering
• 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
• Effective normalization techniques for HOL
• 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
• Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
• 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
• αCheck: A mechanized metatheory model checker
• Beginner's luck: a language for property-based generators
• Unifying theories of programming in Isabelle
• 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
• 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
• 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
• Second-order properties of undirected graphs
• 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
• Detecting inconsistencies in large first-order knowledge bases
• Tests and Proofs for Enumerative Combinatorics
• On logic embeddings and Gödel's God
• Stone relation algebras
• A dyadic deontic logic in HOL

This page was built for software: Nitpick