The following pages link to Nitpick (Q13377):
Displaying 50 items.
- An algebraic approach to computations with progress (Q299188) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- An algebraic approach to multirelations and their properties (Q516032) (← links)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
- Algebras for iteration and infinite computations (Q715050) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- Formally verified algorithms for upper-bounding state space diameters (Q1663245) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- Foundational (co)datatypes and (co)recursion for higher-order logic (Q1687535) (← links)
- Validating mathematical theorems and algorithms with RISCAL (Q1798974) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- Alloy*: a general-purpose higher-order relational constraint solver (Q2009609) (← links)
- Mechanised assessment of complex natural-language arguments using expressive logic combinations (Q2180221) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Infinite executions of lazy and strict computations (Q2347906) (← links)
- On the fine-structure of regular algebra (Q2352506) (← links)
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (Q2360828) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Detecting inconsistencies in large first-order knowledge bases (Q2405258) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Second-order properties of undirected graphs (Q2695354) (← links)
- On Logic Embeddings and Gödel’s God (Q2787333) (← links)
- Model Finding for Recursive Functions in SMT (Q2817915) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Tests and Proofs for Enumerative Combinatorics (Q2827441) (← links)
- HOL Based First-Order Modal Logic Provers (Q2870120) (← links)
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems (Q2945619) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) (Q3058454) (← links)
- Lem: A Lightweight Tool for Heavyweight Semantics (Q3088021) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments (Q3305694) (← links)
- Automating Change of Representation for Proofs in Discrete Mathematics (Q3453117) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
- Closure, Properties and Closure Properties of Multirelations (Q3460617) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- αCheck: A mechanized metatheory model checker (Q4593089) (← links)
