Exploring Theories with a Model-Finding Assistant

DOI10.1007/978-3-319-21401-6_30zbMath1465.68298OpenAlexW1465565820MaRDI QIDQ3454114

Daniel J. Dougherty, Salman Saghafi, Ryan Danas

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_30

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA, CompoSAT: specification-guided coverage for model finding, Pardinus: a temporal relational model finder

Uses Software

• MiniSat
• TPTP
• Darwin
• z3
• E-Darvin
• Mace4
• Kodkod
• iProver-Eq
• iProver
• Razor

Cites Work

• XML queries and constraints, containment and reformulation
• Computing finite models by reduction to function-free clause logic
• Domain theory in logical form
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Positive unit hyperresolution tableaux and their application to minimal model generation
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• A Proof Procedure for Data Dependencies
• A tableau calculus for minimal model reasoning
• Automating Coherent Logic
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Searching for Shapes in Cryptographic Protocols
• Kodkod: A Relational Model Finder
• Unnamed Item
• Unnamed Item
• Unnamed Item