Efficiency of Propositional Proof Systems
A classical question of propositional logic is one of the shortest proof of a tautology. There is a related question of how to construct an algorithm that produces the shortest proof. Cook and Reckhow proposed to attack the NP versus co-NP problem by focusing on lower bounds for standard proof systems of increasing complexity. A related fundamental problem is to determine the relative efficiency of standard proof systems.
First we present an overview of the area paying attention to the relative efficiency of proof systems based on resolution and ordered binary decision diagrams (OBDDs). Resolution is very simple, yet forms the basis of popular tools for theorem proving, such as SAT solvers, that are used in industrial applications. An OBDD is a canonical data structure for symbolic representation of Boolean functions which occurs commonly in formal verification and CAD software for circuit synthesis.
The relative complexity of two proof systems can be measured using the notion of polynomial simulation. Zantema and Groote proved that resolution and OBDDs do not simulate each other polynomially on arbitrary inputs for limited OBDD derivations. However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in conjunctive normal form (CNF). Contrary to popular belief, I will argue that resolution simulates OBDDs polynomially if we limit both to CNFs.
A. Sandler, O. Tveretina: ParaPlan: a Tool for Parallel Reachability Analysis of Planar Polygonal Differential Inclusion Systems, The 8th International Symposium on Games, Automata, Logics, and Formal Verification (Gandalf), 2017
P. Zaichenkov, O. Tveretina, A. Shafarenko: A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces, 12th Int. Conference on integrated Formal Methods (iFM), 2016
P. Zaichenkov, O. Tveretina, A. Shafarenko: Configuring Non-Local Interfaces of Closed-Sourced Cloud Services, iFMCloud'16: The First International Workshop on Formal Methods for and on the Cloud, 2016
P. Zaichenkov, B. Gijsbers, C. Grelck, O. Tveretina, A. Shafarenko: The Cost and Benefits of Coordination Programming: Two Case Studies in Concurrent Collection and S-Net, accepted to Parallel Processing Letters, 2016
P. Zaichenkov, O. Tveretina, A. Shafarenko: Interface Reconciliation in Kahn Process Networks using CSP and SAT, 5th Int. Workshop on the Cross-Fertilization Between CSP and SAT, 2015 [pdf]
P. Zaichenkov, B. Gijsbers, C. Grelck, O. Tveretina, A. Shafarenko: A Case Study in Coordination Programming: S-Net vs Concurrent Collection, In 28th IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW'14) Workshop on Programming Models, Languages and Compilers for Manycore and Heterogeneous Architectures (PLC'14), Phoenix, USA, IEEE Computer Society, 2014 [pdf]
Current research students:
Past research students:
O. Tveretina, D. Funke: Deciding Reachability for 3-Dimensional Multi-Linear Systems. International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011: 250-262
T. Mendt, C. Sinz, O. Tveretina: Probabilistic Model Checking of Constraints in a Supply Chain Business Process. Business Information Systems - 14th International Conference, BIS 2011: 1-12
T. Mendt, C. Sinz, O. Tveretina: Analyzing Separation of Duties Constraints with a Probabilistic Model Checker. BIS (Workshops) 2011: 18-29