Name
Abstract | ||
|---|---|---|
The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. The goal of this paper is to extend Gentzen's sequent calculus to obtain a deductive inference method for FO(ID). The main difficulty in building such a proof system is the representation and inference of unfounded sets. It turns out that we can represent unfounded sets by least fixpoint expressions borrowed from stratified least fixpoint logic (SLFP), which is a logic with a least fixpoint operator and characterizes the expressibility of stratified logic programs. Therefore, in this paper, we integrate least fixpoint expressions into FO(ID) and define the logic FO(ID,SLFP). We investigate a sequent calculus for FO(ID,SLFP), which extends the sequent calculus for SLFP with inference rules for the inductive definitions of FO(ID). We show that this proof system is sound with respect to a slightly restricted fragment of FO(ID) and complete for a more restricted fragment of FO(ID). |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04238-6_13 | LPNMR |
Keywords | Field | DocType |
unfounded set,restricted fragment,fixpoint expression,logic fo,logic programming,deductive system,sequent calculus,stratified logic program,fixpoint logic,order logic,proof system,inference rule,first order logic | Modal μ-calculus,Computer science,Natural deduction,Proof calculus,Sequent calculus,Algorithm,First-order logic,Sequent,Logic programming,Rule of inference | Conference |
Volume | ISSN | Citations |
5753 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 14 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ping Hou | 1 | 5 | 1.41 |
| Marc Denecker | 2 | 1626 | 106.40 |