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
• 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