Finite model finding in first-order modal logics

DOI10.1007/978-3-032-32589-1_20MaRDI QIDQ7411176zbMATH OpenFDO

Authors Happy Khairunnisa Sariyanto, Alexander Steen, Geoff Sutcliffe

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_20

zbMATH Keywords

model findingquantified modal logicTPTP

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• A methodology for hardware verification based on logic simulation
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX '98, Oisterwijk, the Netherlands, May 5--8, 1998. Proceedings
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Dynamic term-modal logics for first-order epistemic planning
• First-order modal logic
• scientific article; zbMATH DE number 1614711 (Why is no real title available?)
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 3148408 (Why is no real title available?)
• scientific article; zbMATH DE number 4208062 (Why is no real title available?)
• scientific article; zbMATH DE number 3499717 (Why is no real title available?)
• scientific article; zbMATH DE number 1028834 (Why is no real title available?)
• scientific article; zbMATH DE number 1765691 (Why is no real title available?)
• scientific article; zbMATH DE number 1765708 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• InKreSAT: modal reasoning via incremental reduction to SAT
• Kodkod: A Relational Model Finder
• Modal and justification logics for multi-agent systems (invited talk)
• Modal logic
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Representation, verification, and visualization of Tarskian interpretations for typed first-order logic
• Semantics-Based Translation Methods for Modal Logics
• Solving quantified modal logic problems by translation to classical logics
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• The logic languages of the TPTP world
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The TPTP World -- infrastructure for automated reasoning
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa
• TPTP, TSTP, CASC, etc.
• Using the TPTP Language for Writing Derivations and Finite Interpretations

This page was built for publication: Finite model finding in first-order modal logics

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