Seminars

Finite Domain Inference Methods for Extensions of First-order Logic
Ping Hou, Visiting SCS-CMU Postdoctoral Fellow

05/16/2011, 2pm, GHC-6501

Abstract

Knowledge representation (KR) is an area in Artificial Intelligence that is concerned with how to use a formal language to represent a domain of discourse. The key problem in KR is to develop formal languages (logics) that can be used to express a wide range of problems, to develop inference methods for these languages, and to develop efficient implementations of these inference methods.

Classical first-order logic (FO) is a base KR-language. In this talk, we introduce two expressive, user-friendly KR-languages, namely, FO(ID) and FO(FD), which are extensions of FO with useful language constructs.

FO(ID), also called ID-Logic, is an extension of FO with inductive definitions, and an integration of FO and logic programming (LP). FO(FD) is an extension of FO with fix-point definitions. The fix-point definition construct in FO(FD) is an integration of LP-style rules and standard fix-point constructs.

 We present the development of finite domain inference engines for FO(ID).

The IDP system is a finite domain model generation system for FO(ID).

In the current state of the art, finite model generation problems are often solved, e.g., in the IDP system, in two phases:

 1. a grounding phase, in which a given first-order theory and a finite domain are reduced to an equivalent variable-free, or propositional, theory;

 2. a propositional model generation phase, in which the models of a given propositional theory are computed.

 The IDP system has similar applications and speed as current Answer Set Programming solvers.

 Another important form of inference for FO(ID) in development is deduction, which is applied to build the proof checker for IDP-system. The deductive systems for FO(ID) are formulated as sequent calculi for a propositional fragment of FO(ID), and for FO(ID), respectively.

 We also present two finite model generation systems for FO(FD). One model generation system for FO(FD) consists of two components: a grounder and a propositional model generator. Another model generation system for

FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic.

 By developing inference methods for these two logics, we want to enhance the understanding of proof-theoretic foundations of them. The proof-theoretic perspectives also allow us to investigate the possibility of FO(ID) and FO(FD) as assertion languages for program verification.

Biography

I am a postdoctoral fellow in the Computer Science Department at Carnegie Mellon University. My research interests lie in logic, automated theorem proving, verification of hybrid systems, logic for hybrid systems, model checking, knowledge representation in logic.

I obtained my Ph.D. in Computer Science from Katholieke Universiteit Leuven, Belgium, and M.E and B.E in Computer Science and Engineering from Nanjing University of Aeronautics and Astronautics, China.