Automated inference of finite unsatisfiability
From MaRDI portal
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
Cites work
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 3614740 (Why is no real title available?)
- scientific article; zbMATH DE number 2090305 (Why is no real title available?)
- Automated Inference of Finite Unsatisfiability
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Solution of the Robbins problem
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- The state of CASC
Cited in
(6)- Automated Inference of Finite Unsatisfiability
- On the use of autarkies for satisfiability decision
- Finding Finite Models in Multi-sorted First-Order Logic
- Encoding monomorphic and polymorphic types
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Deciding simple infinity axiom sets with one binary relation by means of superpostulates
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)