Finding Finite Models in Multi-sorted First-Order Logic

DOI10.1007/978-3-319-40970-2_20zbMath1475.68447arXiv1604.08040OpenAlexW2470240105MaRDI QIDQ2818025

Andrei Voronkov, Martin Suda, Giles Reger

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1604.08040

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Model theory of finite structures (03C13) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Eliminating models during model elimination ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Proving semantic properties as first-order satisfiability ⋮ Old or heavy? Decaying gracefully with age/weight shapes

Uses Software

• MiniSat
• VAMPIRE
• SMT-LIB
• TPTP
• Mace4
• StarExec
• iProver

Cites Work

• Automated inference of finite unsatisfiability
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Sort It Out with Monotonicity
• Theory and Applications of Satisfiability Testing
• Encoding Monomorphic and Polymorphic Types
• Theory and Applications of Satisfiability Testing
• Unnamed Item

This page was built for publication: Finding Finite Models in Multi-sorted First-Order Logic