Title: Formal Decision Making Using Generalized Semantic Games: Applications to Software Development, Research and Education in Formal Science

Speaker: Karl Lieberherr, College of Computer and Information Science, Northeastern University, Boston.

Abstract

We organize formal scientific knowledge in an objectively disputable form and make formal science available to a wider audience. We use generalized semantic games of interpreted logic statements as the foundation for deciding formal science claims. We call the system we built the Scientific Community Game (SCG) which is not only useful as a repository of "clever constructions" but also as a tool for solving computational problems and for research and education in formal science. The role of the user is played by software developers, principal investigators or students, respectively, depending on the application. An impressive application of SCG is a Formal Science Wikipedia.

The generalization of the semantic games includes a new concept, called the Contradiction-Agreement Game, which fairly forces users to play devil's advocate. The generalization also includes a novel way of scaling semantic games to a community of unreliable users. By filtering the noise coming from weak or malicious users, SCG produces a better knowledge base. The filtering is achieved through a voting with justification mechanism. When a user takes a position on a claim, she has to defend that position by winning a semantic game. We describe a proof of concept implementation of SCG which uses a modular construct, called a lab, to group related claims and to solve labs incrementally through lab relations, which are themselves captured as labs. We report on the usage of earlier versions of SCG for teaching software development and algorithms (2007-2012).

A novel feature of SCG is the use of synthetic scholars, with a given skill level, for evaluation. Synthetic users live in labs that are well understood and for which we can create avatars from perfect to dumb ones, forming different skill levels measured by a probability. Synthetic scholars support the experimental evaluation of key properties of SCG before it is given to real users.

SCG internally uses the solution of several computational problems which might currently not be solved optimally. However, we can make an SCG lab out of every such computational problem and use SCG to improve SCG, making SCG a self-improving system.

Joint work with Ahmed Abdelmeged and Yizhou Sun

Short Bio of Speaker:

Karl Lieberherr started his research career in computer science as a theoretical computer scientist, focusing on the theory of P-optimal algorithms for the generalized maximum satisfiability problem (MAX-CSP), still an active area of research. Much later, in 2007, this work has motivated the development of a gaming platform for formal decision making, called the Scientific Community Game (SCG) also known as the Specker Challenge Game, named after former ETH Professor Ernst Specker. He also invented, independently and simultaneously on the other side of the Atlantic (at ETH Zurich), an early form of non-chronological backtracking based on learned clauses (superresolution), which has become a key feature of most state-of-the-art SAT and CSP solvers.

In the mid 1980s, he switched to Object-Oriented and Aspect-Oriented Software Development and focused on issues of software design and modularity. He founded the Demeter research team, which studied the then-novel idea of Adaptive Programming, also known as structure-shy programming and produced the Law of Demeter ("talk only to your friends": an explicit form of coupling control) and several systems for separating concerns in an object-oriented programming context: From Demeter/Flavors to DemeterF.

Dr. Lieberherr is a Professor in the College of Computer and Information Science at Northeastern University.