Monotonicity inference for higher-order formulas

DOI10.1007/s10817-011-9234-1zbMath1266.03021OpenAlexW2018758446MaRDI QIDQ438558

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

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)

Related Items

Encoding Monomorphic and Polymorphic Types, Model Finding for Recursive Functions in SMT

Uses Software

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

Cites Work

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