9th Workshop on Practical Aspects of Automated Reasoning
Home
Important Dates
Call for Papers
Accepted Papers
Proceedings
Program
Registration
Committees
Invited Speakers
Talk: Solution-Counting for Quantified Boolean Formulas
Abstract: In this talk, we survey recent results on counting the numbers of solutions of quantified Boolean formulas (QBFs). In contrast to counting in propositional logic, the solution count for true and false formulas can be calculated dually. We present approaches for counting at the outer quantifier level, counting at the 2nd level, and for arbitrary counting.
Talk: Uniform Substitution.
or: How I Learned to Stop Worrying and Love the Substitution.
Abstract: Virtually every first-rate logician defined the operation of substitution, and almost everyone got it wrong at some point. Uniform substitutions are Alonzo Church’s substitutions that uniformly replace function symbols with terms and predicate symbols with formulas in first-order logic. Uniform substitutions mark the difference between an infinite axiom schema and a finite concrete formula as axioms. This philosophical difference impacts practical theorem provers by being the secret to small soundness-critical prover microkernels. Uniform substitutions replace soundness-critical inference algorithms with mere finite table lookups. With suitable generalizations, uniform substitutions have been shown to succeed in differential dynamic logic for hybrid systems, differential game logic for differential hybrid games, and dynamic logic for communicating hybrid programs. Maybe uniform substitutions can come to a prover near you in the near future?
This talk introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this approach introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms to reason about differential equations. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete. This differential-form differential dynamic logic is the theory behind the KeYmaera X theorem prover, an axiomatic tactical theorem prover for hybrid systems.
References: