Bounded satisfiability checking of FOL^* formulas with aggregations

DOI10.1007/S10703-025-00483-4MaRDI QIDQ6887492zbMATH OpenFDO

Authors Nick Feng, Lina Marsso, Yuliia Kholodetska, Marsha Chechik

Publication date 9 December 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S10703-025-00483-4

zbMATH Keywords

aggregationsatisfiabilitySMT

Mathematics Subject Classification ID

Logic in computer science (03B70) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• Accelerating LTL satisfiability checking by SAT solvers
• Constraint LTL satisfiability checking without automata
• Dynamic magic sets for programs with monotone recursive aggregates
• Early verification of legal compliance via bounded satisfiability checking
• scientific article; zbMATH DE number 1323193 (Why is no real title available?)
• Linear Arithmetic with Stars
• Logic programs with propositional connectives and aggregates
• Model checking software. 14th international SPIN workshop, Berlin, Germany, July 1-3, 2007. Proceedings
• Monitoring metric first-order temporal properties
• Quantifier instantiation techniques for finite model finding in SMT
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Satisfiability checking for mission-time LTL
• Semantics and complexity of recursive aggregates in answer set programming
• Solving \(\mathrm{LIA}^\star\) using approximations
• The ASP system DLV2

This page was built for publication: Bounded satisfiability checking of \(\mathrm{FOL}^*\) formulas with aggregations

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