Automated reasoning with ordinary assertions and default assumptions

Dirk Van Heule; Albert Hoogewijs

doi:10.1109/ISMVL.2001.924572

Automated reasoning with ordinary assertions and default assumptions

Dirk Van Heule, Albert Hoogewijs

Applied Crypto Expertise

University of Ghent

Research output: Contribution to journal › Article › peer-review

Abstract

In this paper, we explain the use of PPC_NAT, a three-valued first-order object logic (PPC) implemented in Isabelle, for reasoning with undefined expressions. This kind of expressions can be found in Default Logic where deductions are divided from facts (which are true) together with a set of assumptions (defaults), which can be true. The main features of our system are: the ability to formalize default assumptions and to reason about them automatically.

Original language	English
Pages (from-to)	193-197
Number of pages	5
Journal	Proceedings of The International Symposium on Multiple-Valued Logic
DOIs	https://doi.org/10.1109/ISMVL.2001.924572
Publication status	Published - 2001

Access to Document

10.1109/ISMVL.2001.924572

Cite this

@article{c9be630835d542a99c9d83207ae8851c,

title = "Automated reasoning with ordinary assertions and default assumptions",

abstract = "In this paper, we explain the use of PPC\_NAT, a three-valued first-order object logic (PPC) implemented in Isabelle, for reasoning with undefined expressions. This kind of expressions can be found in Default Logic where deductions are divided from facts (which are true) together with a set of assumptions (defaults), which can be true. The main features of our system are: the ability to formalize default assumptions and to reason about them automatically.",

author = "\{Van Heule\}, Dirk and Albert Hoogewijs",

year = "2001",

doi = "10.1109/ISMVL.2001.924572",

language = "English",

pages = "193--197",

journal = "Proceedings of The International Symposium on Multiple-Valued Logic",

issn = "0195-623X",

}

TY - JOUR

T1 - Automated reasoning with ordinary assertions and default assumptions

AU - Van Heule, Dirk

AU - Hoogewijs, Albert

PY - 2001

Y1 - 2001

N2 - In this paper, we explain the use of PPC_NAT, a three-valued first-order object logic (PPC) implemented in Isabelle, for reasoning with undefined expressions. This kind of expressions can be found in Default Logic where deductions are divided from facts (which are true) together with a set of assumptions (defaults), which can be true. The main features of our system are: the ability to formalize default assumptions and to reason about them automatically.

AB - In this paper, we explain the use of PPC_NAT, a three-valued first-order object logic (PPC) implemented in Isabelle, for reasoning with undefined expressions. This kind of expressions can be found in Default Logic where deductions are divided from facts (which are true) together with a set of assumptions (defaults), which can be true. The main features of our system are: the ability to formalize default assumptions and to reason about them automatically.

UR - https://www.scopus.com/pages/publications/0034822207

U2 - 10.1109/ISMVL.2001.924572

DO - 10.1109/ISMVL.2001.924572

M3 - Article

AN - SCOPUS:0034822207

SN - 0195-623X

SP - 193

EP - 197

JO - Proceedings of The International Symposium on Multiple-Valued Logic

JF - Proceedings of The International Symposium on Multiple-Valued Logic

ER -

Automated reasoning with ordinary assertions and default assumptions

Abstract

Access to Document

Other files and links

Fingerprint

Cite this