Monotonicity inference for higher-order formulas

DOI10.1007/S10817-011-9234-1zbMATH Open1266.03021OpenAlexW2018758446MaRDI QIDQ438558FDOQ438558

Alexander Krauss, Jasmin Christian Blanchette

Publication date: 31 July 2012

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9234-1

Recommendations

• Monotonicity inference for higher-order formulas
• A monotonicity calculus and its completeness
• scientific article
• Satisfiability modulo bounded checking
• Monotonicity Analysis Can Speed Up Verification

zbMATH Keywords

higher-order logic\texttt{Isabelle/HOL}model finding

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Cites Work

• An introduction to mathematical logic and type theory: To truth through proof.
• A Brief Overview of HOL4
• Title not available (Why is that?)
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Kodkod: A Relational Model Finder
• Verifying a Hotel Key Card System
• Isabelle/HOL. A proof assistant for higher-order logic
• Simplification by Cooperating Decision Procedures
• Sort It Out with Monotonicity
• The small model property: How small can it be?
• Towards a small model theorem for data independent systems in Alloy
• Title not available (Why is that?)
• Logics in Artificial Intelligence
• Monotonicity Inference for Higher-Order Formulas

Cited In (5)

• Model Finding for Recursive Functions in SMT
• Title not available (Why is that?)
• Inductive inference of monotonic formal systems from positive data
• Mapping monotonic restrictions in inductive inference
• Encoding Monomorphic and Polymorphic Types

Uses Software

• Isabelle
• Nitpick
• ML
• Isabelle/HOL
• HOL
• ETPS
• HOL Light
• Kodkod
• Monotonox
• Hotel Key Card

This page was built for publication: Monotonicity inference for higher-order formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438558)