Automated inference of finite unsatisfiability

DOI10.1007/s10817-010-9216-8zbMath1243.68266OpenAlexW2079943511MaRDI QIDQ438540

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

zbMATH Keywords

automated reasoningautomated theorem provingfinite unsatisfiability

Mathematics Subject Classification ID

Related Items (4)

Encoding Monomorphic and Polymorphic Types ⋮ Sort It Out with Monotonicity ⋮ Finding Finite Models in Multi-sorted First-Order Logic ⋮ Deciding simple infinity axiom sets with one binary relation by means of superpostulates

Uses Software

• SPASS
• TPTP
• Mace4
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solution of the Robbins problem
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Automated Inference of Finite Unsatisfiability

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