Name
Abstract | ||
|---|---|---|
This work is about a “real-world” application of automated deduction. The application is the management of documents (such
as mathematical textbooks) as they occur in a readily available tool. These documents are “living”, in the sense, that they
can be modified and extended by the reader, who can interact via Living Books with external systems.
A particular task is to assemble a new document from such units in a selective way, based on the user’s current interest and
knowledge.
It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited
for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose
a model computation theorem prover as a suitable deduction mechanism.
|
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/978-3-540-32254-2_15 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
first order,theorem prover,automated deduction | Judgment,Programming language,Computer science,Automated theorem proving,Sequent calculus,Algorithm,Non-monotonic logic,Constraint logic programming | Conference |
Volume | ISSN | Citations |
2605 | 0302-9743 | 2 |
PageRank | References | Authors |
0.40 | 21 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Baumgartner | 1 | 364 | 26.97 |
| Ulrich Furbach | 2 | 639 | 88.23 |
| Dieter Hutter | 3 | 449 | 55.74 |
| werner stephan | 4 | 17 | 1.64 |