Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
From MaRDI portal
Publication:5747646
DOI10.1007/978-3-642-14052-5_11zbMath1291.68326OpenAlexW1595209293MaRDI QIDQ5747646
Tobias Nipkow, Jasmin Christian Blanchette
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_11
Related Items
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, Stone Relation Algebras, Automating change of representation for proofs in discrete mathematics (extended version), Tests and proofs for custom data generators, An algebraic approach to computations with progress, Automatic Proof and Disproof in Isabelle/HOL, 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, Instrumenting a weakest precondition calculus for counterexample generation, Computational logic: its origins and applications, 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, Extensional higher-order paramodulation in Leo-III, Formalizing Ordinal Partition Relations Using Isabelle/HOL, Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems, A bi-directional extensible interface between Lean and Mathematica, Unifying Theories of Programming in Isabelle, A Hierarchy of Algebras for Boolean Subsets, Computer-Supported Exploration of a Categorical Axiomatization of Modeloids, Computer-Supported Analysis of Arguments in Climate Engineering, LOGICS OF FORMAL INCONSISTENCY ENRICHED WITH REPLACEMENT: AN ALGEBRAIC AND MODAL ACCOUNT, Automated Kantian ethics: a faithful implementation, Alien coding, αCheck: A mechanized metatheory model checker, Constraint solving for finite model finding in SMT solvers, The 11th IJCAR automated theorem proving system competition – CASC-J11, The MET: The Art of Flexible Reasoning with Modalities, Solving modal logic problems by translation to higher-order logic, Formalising basic topology for computational logic in simple type theory, Unnamed Item, Quantified multimodal logics in simple type theory, Second-order properties of undirected graphs, Higher-Order Modal Logics: Automation and Applications, Monotonicity inference for higher-order formulas, Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, A Lambda-Free Higher-Order Recursive Path Order, Unnamed Item, Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments, An algebraic approach to multirelations and their properties, Verifying minimum spanning tree algorithms with Stone relation algebras, Computer-assisted analysis of the Anderson-Hájek ontological controversy, Alloy*: a general-purpose higher-order relational constraint solver, Monotonicity Inference for Higher-Order Formulas, Algebras for iteration and infinite computations, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), 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, Model Finding for Recursive Functions in SMT, Effective Normalization Techniques for HOL, Nitpick, Tests and Proofs for Enumerative Combinatorics, Semantics of Mizar as an Isabelle object logic, Infinite executions of lazy and strict computations, On the fine-structure of regular algebra
Uses Software
