Classical logic with partial functions

Hans De Nivelle

doi:10.1007/978-3-642-14203-1_18

Classical logic with partial functions

Hans De Nivelle

University of Wrocław

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Citations (Scopus)

Abstract

We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.

Original language	English
Title of host publication	Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings
Pages	203-217
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-14203-1_18
Publication status	Published - 2010
Externally published	Yes
Event	5th International Joint Conference on Automated Reasoning, IJCAR 2010 - Edinburgh, United Kingdom Duration: Jul 16 2010 → Jul 19 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6173 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Joint Conference on Automated Reasoning, IJCAR 2010
Country/Territory	United Kingdom
City	Edinburgh
Period	7/16/10 → 7/19/10

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-14203-1_18

Cite this

Classical logic with partial functions. / De Nivelle, Hans.
Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. 2010. p. 203-217 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6173 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

De Nivelle, H 2010, Classical logic with partial functions. in Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6173 LNAI, pp. 203-217, 5th International Joint Conference on Automated Reasoning, IJCAR 2010, Edinburgh, United Kingdom, 7/16/10. https://doi.org/10.1007/978-3-642-14203-1_18

@inproceedings{4a77b342124348129ef176cf5a6058af,

title = "Classical logic with partial functions",

abstract = "We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.",

author = "\{De Nivelle\}, Hans",

year = "2010",

doi = "10.1007/978-3-642-14203-1\_18",

language = "English",

isbn = "3642142028",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "203--217",

booktitle = "Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings",

note = "5th International Joint Conference on Automated Reasoning, IJCAR 2010 ; Conference date: 16-07-2010 Through 19-07-2010",

}

TY - GEN

T1 - Classical logic with partial functions

AU - De Nivelle, Hans

PY - 2010

Y1 - 2010

N2 - We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.

AB - We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.

UR - http://www.scopus.com/inward/record.url?scp=77955240470&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77955240470&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14203-1_18

DO - 10.1007/978-3-642-14203-1_18

M3 - Conference contribution

AN - SCOPUS:77955240470

SN - 3642142028

SN - 9783642142024

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 203

EP - 217

BT - Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings

T2 - 5th International Joint Conference on Automated Reasoning, IJCAR 2010

Y2 - 16 July 2010 through 19 July 2010

ER -

Classical logic with partial functions

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this