Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:30 - 18:45 at VMCAI - Decision Procedures Chair(s): Alexander J. Summers

Simple clause learning over theories SCL(T) is a decision procedure for the Bernays-Schoenfinkel fragment over bounded difference constraints BS(BD). The BS(BD) fragment consists of clauses built from first-order literals without function symbols together with simple bounds or difference constraints, where for the latter it is required that the variables of the difference constraint are bounded from below and above. The SCL(T) calculus builds model assumptions over a fixed finite set of fresh constants. The model assumptions consist of ground foreground first-order and ground background theory literals. The model assumptions guide inferences on the original clauses with variables. We prove that all clauses generated this way are non-redundant. As a consequence, expensive testing for tautologies and forward subsumption is completely obsolete and termination with respect to a fixed finite set of constants is a consequence. We prove SCL(T) to be sound and refutationally complete for the combination of the the Bernays Schoenfinkel fragment with any compact theory. Refutational completeness is obtained by enlarging the set of considered constants. For the case of BS(BD) we prove an abstract finite model property such that the size of a sufficiently large set of constants can be fixed a priori.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. SummersUniversity of British Columbia
18:30
15m
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF
Media Attached
18:45
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen HoenickeUniversity of Freiburg, Tanja SchindlerUniversity of Freiburg
Media Attached
19:00
15m
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg
Media Attached
19:15
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc LeUniversity College London, UK
Media Attached