The field of formal verification and logic is moving towards the development of more expressive and powerful formal systems, allowing for the direct expression of arbitrary recursive definitions and the incorporation of uncertain information. Researchers are exploring new techniques, such as dynamic typing and syntactic concept lattice models, to mitigate issues with completeness and decidability in various logics. Noteworthy papers include: Possibilistic Computation Tree Logic, which introduces a complete axiomatization of PoCTL and shows that the satisfiability problem is decidable in exponential time. The paper on grounded arithmetic presents a minimalistic foundation for formal reasoning that allows the direct expression of arbitrary recursive definitions. The work on uniform interpolation property in multi-agent modal logic establishes a purely syntactic algorithm for determining a uniform interpolant formula.
Advances in Formal Verification and Logic
Sources
Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization
Proceedings of the Combined 32nd International Workshop on Expressiveness in Concurrency and 22nd Workshop on Structural Operational Semantics
On the entailment problem for DL-Lite$_{core}$ ontologies and conjunctive queries with negation
On syntactic concept lattice models for the Lambek calculus and infinitary action logic
Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
A proof-theoretic approach to uniform interpolation property of multi-agent modal logic
Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
Finding Regular Herbrand Models for CHCs using Answer Set Programming
Semantic Properties of Computations Defined by Elementary Inference Systems
Theta as a Horn Solver
CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses