Automated inference of finite unsatisfiability

DOI10.1007/S10817-010-9216-8zbMATH Open1243.68266OpenAlexW2079943511MaRDI QIDQ438540FDOQ438540

Ann Lillieström, Koen Claessen

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-010-9216-8

Recommendations

• Automated Inference of Finite Unsatisfiability
• Automated Model Building: From Finite to Infinite Models
• Finite Quantification in Hierarchic Theorem Proving
• Finite model finding using the logic of equality with uninterpreted functions
• A new method for automated finite model building exploiting failures and symmetries

zbMATH Keywords

automated reasoningautomated theorem provingfinite unsatisfiability

Mathematics Subject Classification ID

Cites Work

• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Solution of the Robbins problem
• The state of CASC
• Automated Inference of Finite Unsatisfiability

Cited In (6)

• Automated Inference of Finite Unsatisfiability
• Sort It Out with Monotonicity
• On the use of autarkies for satisfiability decision
• Finding Finite Models in Multi-sorted First-Order Logic
• Encoding Monomorphic and Polymorphic Types
• Deciding simple infinity axiom sets with one binary relation by means of superpostulates

Uses Software

• SPASS
• TPTP
• Mace4
• E Theorem Prover

This page was built for publication: Automated inference of finite unsatisfiability

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