Model Evolution-Based Theorem Proving

Peter Baumgartner

doi:10.1109/MIS.2013.124

Model Evolution-Based Theorem Proving

Peter Baumgartner^*

^*Corresponding author for this work

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

2 Citations (Scopus)

Abstract

Peter Baumgartner highlights two trends that have received considerable attention in the field of automated theorem proving. The area of automated theorem proving is characterized by the development of numerous calculi and proof procedures, ranging from general purpose to specialized ones for specific subsets of first-order logic and logical theories. One of trends involves the integration of reasoning methods for propositional and for first-order logic, with a best-of-both-worlds motivation. The other trend involves built-in reasoning support modulo background theories, such as equality and integer arithmetic, which are important for software verification applications.

Original language	English
Pages (from-to)	4-10
Number of pages	7
Journal	IEEE Intelligent Systems
Volume	29
Issue number	1
DOIs	https://doi.org/10.1109/MIS.2013.124
Publication status	Published - 2014
Externally published	Yes

Access to Document

10.1109/MIS.2013.124

Cite this

@article{d412caceedd44263b9cf3ebff79a5b7e,

title = "Model Evolution-Based Theorem Proving",

abstract = "Peter Baumgartner highlights two trends that have received considerable attention in the field of automated theorem proving. The area of automated theorem proving is characterized by the development of numerous calculi and proof procedures, ranging from general purpose to specialized ones for specific subsets of first-order logic and logical theories. One of trends involves the integration of reasoning methods for propositional and for first-order logic, with a best-of-both-worlds motivation. The other trend involves built-in reasoning support modulo background theories, such as equality and integer arithmetic, which are important for software verification applications.",

keywords = "automated reasoning, automated theorem proving, intelligent systems, knowledge representation",

author = "Peter Baumgartner",

year = "2014",

doi = "10.1109/MIS.2013.124",

language = "English",

volume = "29",

pages = "4--10",

journal = "IEEE Intelligent Systems",

issn = "1541-1672",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "1",

}

TY - JOUR

T1 - Model Evolution-Based Theorem Proving

AU - Baumgartner, Peter

PY - 2014

Y1 - 2014

N2 - Peter Baumgartner highlights two trends that have received considerable attention in the field of automated theorem proving. The area of automated theorem proving is characterized by the development of numerous calculi and proof procedures, ranging from general purpose to specialized ones for specific subsets of first-order logic and logical theories. One of trends involves the integration of reasoning methods for propositional and for first-order logic, with a best-of-both-worlds motivation. The other trend involves built-in reasoning support modulo background theories, such as equality and integer arithmetic, which are important for software verification applications.

AB - Peter Baumgartner highlights two trends that have received considerable attention in the field of automated theorem proving. The area of automated theorem proving is characterized by the development of numerous calculi and proof procedures, ranging from general purpose to specialized ones for specific subsets of first-order logic and logical theories. One of trends involves the integration of reasoning methods for propositional and for first-order logic, with a best-of-both-worlds motivation. The other trend involves built-in reasoning support modulo background theories, such as equality and integer arithmetic, which are important for software verification applications.

KW - automated reasoning

KW - automated theorem proving

KW - intelligent systems

KW - knowledge representation

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

U2 - 10.1109/MIS.2013.124

DO - 10.1109/MIS.2013.124

M3 - Article

SN - 1541-1672

VL - 29

SP - 4

EP - 10

JO - IEEE Intelligent Systems

JF - IEEE Intelligent Systems

IS - 1

ER -

Model Evolution-Based Theorem Proving

Abstract

Access to Document

Other files and links

Fingerprint

Cite this