International Center for Computational Logic - Benutzerbeiträge [de]

Inproceedings3150

2018-02-15T09:07:14Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=The Boolean Solution Problem from the Perspective of Predicate Logic
|To appear=0
|Year=2017
|Booktitle=11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
|Pages=333-350
|Publisher=Springer
|Editor=Clare Dixon, Marcelo Finger
|Series=LNCS (LNAI)
|Volume=10483
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3037/en

2018-02-15T09:03:22Z

Christoph Wernhard: Page created automatically by parser function on page Techreport3037

#REDIRECT [[Techreport3037]]

Techreport3037

2018-02-15T09:03:22Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Techreport |Title= Craig Interpolation and Access Interpolation wit…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title= Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux
|Year=2018
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning
|Archivierungsnummer=18-01
}}
{{Publikation Details
|Link=https://arxiv.org/abs/1802.04982
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3023

2017-12-20T06:55:36Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
|Year=2015
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning
|Archivierungsnummer=15-05
}}
{{Publikation Details
|Link=https://arxiv.org/abs/1712.06868
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3192/en

2017-12-09T20:11:34Z

Christoph Wernhard: Page created automatically by parser function on page Inproceedings3192

#REDIRECT [[Inproceedings3192]]

Inproceedings3192

2017-12-09T20:11:34Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Inproceedings |Referiert=1 |Title=Approximating Resultants of Exist…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas
|To appear=0
|Year=2017
|Booktitle=Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)
|Pages=82-98
|Publisher=CEUR-WS.org
|Editor=Patrick Koopmann, Sebastian Rudolph, Renate A. Schmidt, Christoph Wernhard
|Series=CEUR Workshop Proceedings
|Volume=2013
}}
{{Publikation Details
|ISSN=1613-0073
|Link=http://ceur-ws.org/Vol-2013/paper17.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Misc3029

2017-12-09T20:04:58Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Misc |Title=Craig Interpolation and Query Reformulation with Clausa…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Misc
|Title=Craig Interpolation and Query Reformulation with Clausal First-Order Tableaux
|Year=2017
|Month=September
|Howpublished=Poster presentation at TABLEAUX 2017, Brasilia
}}
{{Publikation Details
|Link=http://cs.christophwernhard.com/papers/tableaux_2017_poster.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Proceedings3013

2017-12-09T19:57:26Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Patrick
|ErsterAutorNachname=Koopmann
|FurtherAuthors=Sebastian Rudolph; Renate A. Schmidt; Christoph Wernhard;
}}
{{Proceedings
|Title=Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)
|To appear=0
|Year=2017
|Publisher=CEUR-WS.org
|Series=CEUR Workshop Proceedings
|Volume=2013
}}
{{Publikation Details
|ISSN=1613-0073
|Link=http://ceur-ws.org/Vol-2013/
|Projekt=SOA-VBQP
|Forschungsgruppe=Automatentheorie, Computational Logic, Wissensverarbeitung
}}

Proceedings3013

2017-12-09T19:55:56Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Patrick
|ErsterAutorNachname=Koopmann
|FurtherAuthors=Sebastian Rudolph; Renate A. Schmidt; Christoph Wernhard
}}
{{Proceedings
|Title=Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)
|To appear=0
|Year=2017
|Publisher=CEUR-WS.org
|Series=CEUR Workshop Proceedings
|Volume=2013
}}
{{Publikation Details
|ISSN=1613-0073
|Link=http://ceur-ws.org/Vol-2013/
|Projekt=SOA-VBQP
|Forschungsgruppe=Automatentheorie, Computational Logic, Wissensverarbeitung
}}

Proceedings3013/en

2017-12-09T19:49:27Z

Christoph Wernhard: Page created automatically by parser function on page Proceedings3013

#REDIRECT [[Proceedings3013]]

Proceedings3013

2017-12-09T19:49:27Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Patrick |ErsterAutorNachname=Koopmann |FurtherAuthors=Sebastian Rudolph, Renate A. Schmidt, Christoph Wernhard }…“

{{Publikation Erster Autor
|ErsterAutorVorname=Patrick
|ErsterAutorNachname=Koopmann
|FurtherAuthors=Sebastian Rudolph, Renate A. Schmidt, Christoph Wernhard
}}
{{Proceedings
|Title=Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)
|To appear=0
|Year=2017
|Publisher=CEUR-WS.org
|Series=CEUR Workshop Proceedings
|Volume=2013
}}
{{Publikation Details
|ISSN=1613-0073
|Link=http://ceur-ws.org/Vol-2013/
|Projekt=SOA-VBQP
|Forschungsgruppe=Automatentheorie, Computational Logic, Wissensverarbeitung
}}

SOQE 2017

2017-09-13T10:43:47Z

Christoph Wernhard:

{{Veranstaltung
|Titel EN=SOQE 2017: Workshop on Second-Order Quantifier Elimination and Related Topics
|Beschreibung EN=Workshop on Second-Order Quantifier Elimination and Related Topics
|Veranstaltungsart=Konferenz
|Start=2017/12/06 09:00:00
|Ende=2017/12/08 18:00:00
|URL=http://2017.soqe.org/
|Forschungsgruppe=Automatentheorie, Computational Logic, Wissensverarbeitung
|In News anzeigen=1
}}

SOQE 2017/en

2017-09-13T10:42:06Z

Christoph Wernhard: Page created automatically by parser function on page SOQE 2017

SOQE 2017

2017-09-13T10:42:05Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=SOQE 2017 |Beschreibung EN=Workshop on Second-Order Quantifier Elimination and Related Topics |Veranstaltungsart=Konferenz |Start=201…“

{{Veranstaltung
|Titel EN=SOQE 2017
|Beschreibung EN=Workshop on Second-Order Quantifier Elimination and Related Topics
|Veranstaltungsart=Konferenz
|Start=2017/12/06 09:00:00
|Ende=2017/12/08 18:00:00
|URL=http://2017.soqe.org/
|Forschungsgruppe=Automatentheorie, Computational Logic, Wissensverarbeitung
|In News anzeigen=1
}}

News30

2017-07-24T05:34:18Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Happy Birthday Steffen! |Titel EN=Happy Birthday Steffen! |Beschreibung DE=Happy birthday to ICCL co-founder Steffen Hölldobler who cele…“

{{Neuigkeit
|Titel DE=Happy Birthday Steffen!
|Titel EN=Happy Birthday Steffen!
|Beschreibung DE=Happy birthday to ICCL co-founder Steffen Hölldobler who celebrates his 60th birthday today.

|Beschreibung EN=Happy birthday to ICCL co-founder Steffen Hölldobler who celebrates his 60th birthday today.

|Datum=2017/07/22
}}

SOA-VBQP

2017-07-10T13:20:51Z

Christoph Wernhard:

{{Projekt
|Kurzname=SOA-VBQP
|Name=Der Second-Order Ansatz und dessen Anwendung in der Sicht-basierten Anfrageverarbeitung
|Name EN=The Second-Order Approach and its Application to View-Based Query Processing
|Beschreibung DE=Im Projekt wird ein Ansatz zur Logik-basierten Wissensverarbeitung untersucht, der hier Second-Order Ansatz genannt werden soll. Die Idee ist, dass ausdrucksstarke Repräsentationssprachen einerseits verfügbar sind, um Anwendungen auf sehr natürliche Art zu formulieren, andererseits aber durch Reduktion auf schwächere Sprachen verarbeitet werden, die sich besser zur Berechnung eignen. Solche Reduktionen werden durch die Verwendung der ausdrucksstarken Sprachkonstrukte in spezifischen Anwendungskontexten ermöglicht.

Proofs of Concept für diesen Ansatz wurden in den späten 90er Jahren mit dem Einsatz der Elimination von Quantoren zweiter Stufe zur Zirkumskriptionsberechnung und in letzter Zeit mit Anwendungen der uniformen Interpolation (die sich als Elimination von Quantoren zweiter Stufe ausdrücken lässt) in Beschreibungslogiken vorgelegt. Der Ansatz erlaubt es typischerweise, Konzepte aus dem Anwendungsbereich auf grundlegende Konzepte der Logik zurückzuführen und damit neue Anwendungsmöglichkeiten sowie Parallelen zwischen Gebieten, die den Austausch und die Kombination von Techniken ermöglichen, aufzuzeigen.

Das Projekt verbindet zwei Arbeitslinien, die sich gegenseitig anregen: (1) Konzepte aus einem bestimmten Anwendungsbereich, der Sicht-basierten Anfrageverarbeitung, werden formal mit Operatoren zweiter Stufe modelliert. (2) Berechnungsmethoden werden entwickelt, die Anwendungen auf Grundlage der Formalisierung und im Wesentlichen durch Elimination von Operatoren zweiter Stufe realisieren.

Grundidee der Sicht-basierten Anfrageverarbeitung ist, Anfragen zu übersetzen und zu zerlegen, so dass mehrere Agenten mit spezialisierten Wissensbasen und Verarbeitungsfähigkeiten zur Antwortberechnung beitragen können. Sicht-basierte Anfrageverarbeitung ist durch den engen Bezug zu Definierbarkeit, einem allgemeinen Konzept der Logik, für den Ansatz des Projekts gut geeignet. Projektziele bezüglich der Sicht-basierten Anfrageverarbeitung sind semantische Klärung der beteiligten Konzepte, Erschließung der Elimination von Operatoren zweiter Stufe zur Berechnung von Anfragetransformationen sowie Generalisierung über Datenbanken hinaus.

In Bezug auf Berechnungsmethoden sollen neue Techniken zur Elimination von Quantoren zweiter Stufe entwickelt werden, basierend auf Aussagenlogik - verwandt mit aktuellen SAT-Präprozessoren, basierend auf Prädikatenlogik erster Stufe, sowie durch Berücksichtigung spezifischer Formelmuster, die in der Sicht-basierten Anfrageverarbeitung vorkommen.

Die Projektergebnisse sollen als ausgearbeitete formale und automatisierte Grundlage für eine Vielzahl von weiteren für den Second-Order Ansatz geeigneten Anwendungen dienen. Dazu gehören beispielsweise Varianten von nicht-standard Inferenzen, abduktives Schließen, Modularisierung von Wissensbasen, nicht-monotones Schließen und Schließen über Wissen.
|Beschreibung EN=In the project, an approach to logic-based knowledge processing, to be called here second-order approach, will be investigated. The idea is that expressive representation languages are, on the one hand, available to formulate applications in a very natural way, but on the other hand, are processed by reduction to poorer languages that are better suited for computation. Such reductions are made possible because the expressive language constructs are used in specific application contexts.

Proofs of concept for this approach have been given in the late 90s with the use of second-order quantifier elimination for computing circumscription, and recently with applications of uniform interpolation (which can be expressed as second-order quantifier elimination) in description logics. The approach typically allows to trace concepts from the application area back to fundamental concepts of logic, indicating new application possibilities and parallels between areas that enable transfer and combination of techniques.

The project connects two lines of work that will stimulate each other: (1) Concepts of a particular application area, view-based query processing, will be formally modeled with second-order operators. (2) Computational methods will be developed that realize applications, on the basis of the formalization, essentially by elimination of second-order operators.

The basic idea of view-based query processing is to translate and decompose queries such that multiple agents with specialized knowledge bases and processing capabilities can contribute to answer computation. By its is close relation to definability, a general concept of logic, view-based query processing is well suited to the approach of the project. Central objectives of the project with respect to view-based query processing are semantic clarification of the involved concepts, availability of second-order operator elimination to compute query transformations, and generalization beyond databases.

With respect to computational methods, new techniques for second-order operator elimination will be developed, based on propositional logic - related to recent SAT preprocessors, based on first-order logic, and by taking specific formula patterns into account that occur in view-based query processing.

The results of the project should serve as an elaborate formal and automated foundation for a multitude of further applications that are suited for the second-order approach. These include, for example, variants of non-standard inferences, abductive reasoning, modularization of knowledge bases, non-monotonic reasoning, and reasoning about knowledge.
|Kontaktperson=Christoph Wernhard
|URL=http://cs.christophwernhard.com/projects/soa/
|Start=2015/04/01
|Finanziert von=DFG
|Projektstatus=aktiv
|Person=Christoph Wernhard, Walter Forkel, Elias Werner
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3034/en

2017-06-27T05:32:17Z

Christoph Wernhard: Page created automatically by parser function on page Techreport3034

#REDIRECT [[Techreport3034]]

Techreport3034

2017-06-27T05:32:17Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Techreport |Title=The Boolean Solution Problem from the Perspective…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=The Boolean Solution Problem from the Perspective of Predicate Logic – Extended Version
|Year=2017
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning
|Archivierungsnummer=17-01
}}
{{Publikation Details
|Link=https://arxiv.org/abs/1706.08329
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3150/en

2017-06-14T09:19:04Z

Christoph Wernhard: Page created automatically by parser function on page Inproceedings3150

#REDIRECT [[Inproceedings3150]]

Inproceedings3150

2017-06-14T09:19:03Z

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=The Boolean Solution Problem from the Perspective of Predicate Logic
|To appear=1
|Year=2017
|Booktitle=11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
|Publisher=Springer
|Editor=Clare Dixon, Marcelo Finger
|Series=LNCS (LNAI)
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

SOA-VBQP

2016-10-07T12:49:19Z

Christoph Wernhard:

MCL/IntroductoryWeek

2016-10-03T17:58:53Z

Christoph Wernhard: Link zu "How to write a research paper" auf neues PDF writing2016.pdf gesetzt.

{{#leftsidenav:

{{LeftsidenavHeading|[[MCL/en|International Master]]}}

<ul class="nav-list">
<li>[[MCL/Introduction/en|Introduction]]</li>

<li>[[MCL/For_Prospective_Students/en|For Prospective Students]]</li>

<li>[[MCL/CurrentStudents/en|For Current Students]]</li>

<div style="font-size: 95%; padding-bottom: 1ex !important; ">
<ul class="nav-list" style="padding-left: 1ex !important; ">
<li>[[MCL/Courses/WS2016/en|Courses]]</li>

<li>[[MCL/Timetable/WS2016/en|Timetable]]</li>

<li>[[MCL/Social_Events/en|Social Events]]</li>

<li>[[MCL/CurrentStudents/Financial_Support/en|Financial Support]]</li>

<li>[[MCL/CurrentStudents/Other_Information/en|Other Information]]</li>
</ul>
</div>

<li>[[MCL/Business_Industry/en|Business and Industry]]</li>

<li>[[MCL/Grants/en|Grants]]</li>

<li>[[MCL/Guests_Events/en|Guests and Events]]</li>

<li>[[MCL/Internals/en|Internals]]</li>
</ul>

__NOTOC__
|

{{Main heading|Introductory Week for CL Students}}

You find the schedule of the week [[Datei:plan-2016.pdf]]

== Slides ==
* How to give a research talk – Emmanuelle Dietz [https://ddll.inf.tu-dresden.de/w/images/a/a5/A-TALK-ON-GIVING-TALKS-I-beamer-emma.pdf part I] [https://ddll.inf.tu-dresden.de/w/images/d/d3/A-TALK-ON-GIVING-TALKS-II-beamer-emma.pdf part II]
* [http://www.wv.inf.tu-dresden.de/~wernhard/teaching/writing2016.pdf How to write a research paper – Christoph Wernhard]
* [https://ddll.inf.tu-dresden.de/w/images/6/65/LatexIntro.pdf Introduction to LaTeX – Peter Steinke]
* [https://ddll.inf.tu-dresden.de/w/images/5/5a/Beamer-intro.pdf Introduction to Beamer] – Tobias Philipp

* Introduction to [https://ddll.inf.tu-dresden.de/w/images/4/4a/Tikz-introduction-2015.pdf TikZ] and [https://ddll.inf.tu-dresden.de/w/images/0/0f/Git-introduction-2015.pdf GIT] – Sibylle Möhle

== City Tour ==
The city tour starts at tram station Prager Straße on 1pm. 
There are English-speaking guides!

 
}}

Inproceedings3065

2016-07-11T17:10:58Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard;
}}
{{Inproceedings
|Referiert=1
|Title=Towards Knowledge-Based Assistance for Scholarly Editing
|To appear=0
|Year=2016
|Booktitle=1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016 (Book of Abstracts)
|Pages=29-31
|Editor=Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, Josef Urban
}}
{{Publikation Details
|Link=http://aitp-conference.org/aitp_proceedings.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3096

2016-07-11T17:05:24Z

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=The PIE system for Proving, Interpolating and Eliminating
|To appear=0
|Year=2016
|Booktitle=5th Workshop on Practical Aspects of Automated Reasoning (PAAR)
|Pages=125-138
|Editor=Pascal Fontaine, Stephan Schulz, Josef Urban
|Series=CEUR Workshop Proceedings
|Volume=1635
}}
{{Publikation Details
|Link=http://ceur-ws.org/Vol-1635/#paper-11
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3064

2016-03-17T09:26:07Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Knowledge-Based Support for Scholarly Editing and Text Processing
|To appear=0
|Year=2016
|Booktitle=DHd 2016 – Digital Humanities im deutschsprachigen Raum: Modellierung – Vernetzung – Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma. Konferenzabstracts.
|Pages=176-179
|Publisher=nisaba verlag
}}
{{Publikation Details
|Link=http://dhd2016.de/boa.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3065

2016-01-03T14:39:14Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard;
}}
{{Inproceedings
|Referiert=1
|Title=Towards Knowledge-Based Assistance for Scholarly Editing
|To appear=1
|Year=2016
|Booktitle=1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016 (Book of Abstracts)
|Editor=Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, Josef Urban
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3065

2016-01-03T14:14:00Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard;
}}
{{Inproceedings
|Referiert=1
|Title=Towards Knowledge-Based Assistance for Scholarly Editing
|To appear=1
|Year=2016
|Booktitle=1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016
|Editor=Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, Josef Urban
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3064

2016-01-03T14:11:04Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Knowledge-Based Support for Scholarly Editing and Text Processing
|To appear=1
|Year=2016
|Booktitle=3. Konferenz des Fachverbandes "Digital Humanities im deutschsprachigen Raum" DHd 2016 "Modellierung - Vernetzung - Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma"
|Editor=Johannes Stigler
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3065/en

2016-01-03T13:58:49Z

Christoph Wernhard: Page created automatically by parser function on page Inproceedings3065

#REDIRECT [[Inproceedings3065]]

Inproceedings3065

2016-01-03T13:58:45Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Jana |ErsterAutorNachname=Kittelmann |FurtherAuthors=Christoph Wernhard; }} {{Inproceedings |Referiert=1 |Title…“

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard;
}}
{{Inproceedings
|Referiert=1
|Title=Towards Knowledge-Based Assistance for Scholarly Editing
|To appear=1
|Year=2016
|Booktitle=1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3064/en

2015-12-29T10:21:51Z

Christoph Wernhard: Page created automatically by parser function on page Inproceedings3064

#REDIRECT [[Inproceedings3064]]

Inproceedings3064

2015-12-29T10:21:48Z

{{Publikation Erster Autor
|ErsterAutorVorname=Jana
|ErsterAutorNachname=Kittelmann
|FurtherAuthors=Christoph Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Knowledge-Based Support for Scholarly Editing and Text Processing
|To appear=1
|Year=2016
|Booktitle=3. Konferenz des Fachverbandes "Digital Humanities im deutschsprachigen Raum" DHd 2016 "Modellierung - Vernetzung - Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma"
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Formale Systeme(WS2015)

2015-11-07T08:02:00Z

Christoph Wernhard:

{{Vorlesung
|Title=Formale Systeme
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler
|Tutors=Emmanuelle Dietz; Tobias Philipp; Peter Steinke;
|Term=WS
|Year=2015
|Module=INF-B-270, INF-B-275, INF-LE-EUI, IST-05-PF-HS
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=Klausur
|Description=<center> 
== Die Übung am Montag 6.DS findet ab jetzt immer in APB/E010 statt! ==
 
==Die Übungen am Montag und am Dienstag in der 1.DS fallen aus!==
</center>

 

=Übungen =

Folgende Übungsgruppen finden statt:
* 6. DS Montag APB/E010
* 2. DS Dienstag APB/E001
* 1. DS Mittwoch APB/E001
* 6. DS Mittwoch APB/E009
* 1. DS Donnerstag APB/E008
* 1. DS Freitag WIL/C203
* 2. DS Freitag APB/E008
* 3. DS Freitag APB/E006
* 3. DS Freitag SCH/A252
* 5. DS Freitag APB/E010

== Übungsblätter ==

* [https://ddll.inf.tu-dresden.de/w/images/b/b2/Fs_01.pdf 1.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/d/d5/Fs_02.pdf 2.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/f/fa/Fs_03.pdf 3.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/3/3c/Fs_04.pdf 4.Übungsblatt]

=Vorlesung=

* Die Vorlesung findet montags in der 3. DS in HSZ02 und donnerstags in der 4. DS in HSZ03 statt (ausser zwischen dem 21.12.2015 und dem 03.01.2016)

== Vorlesungsfolien ==

* [https://ddll.inf.tu-dresden.de/w/images/5/5d/FS-2015-einf%C3%BChrung.pdf Einführung]
* [https://ddll.inf.tu-dresden.de/w/images/c/c4/FS-2015-geschichte.pdf Geschichte der Logik]
* [https://ddll.inf.tu-dresden.de/w/images/c/cc/FS-2015-aussagenlogik.pdf Aussagenlogik]

== Weitere Folien ==

* [https://ddll.inf.tu-dresden.de/w/images/0/04/Al_ergaenzung.pdf Aussagenlogik: Ergänzungen 5.11.2015]
* [https://ddll.inf.tu-dresden.de/w/images/5/54/Beispiel_endlichkeitssatz.pdf Aussagenlogik: Beispiel zum Endlichkeitssatz 5.11.2015]
|Literature=Der erste Teil der Vorlesung basiert auf die folgenden Bücher:

S. Hölldobler: Logik und Logikprogrammierung. Synchron Publishers GmbH, Heidelberg (2009). ISBN 978-3-935025-84-3
[http://www.wv.inf.tu-dresden.de/Teaching/WS-2012/formsys/Korr-Lehrbuch.pdf Korrekturen und Anmerkungen zu diesem Buch]

S. Hölldobler, S. Bader, B. Fronhöfer, U. Hans, P. Hitzler, M. Krötzsch, T. Pietzsch: : Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen; Synchron Publishers GmbH, Heidelberg (2011). ISBN 978-3-935025-85-0
}}

Formale Systeme(WS2015)

2015-11-07T08:00:13Z

Christoph Wernhard:

{{Vorlesung
|Title=Formale Systeme
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler
|Tutors=Emmanuelle Dietz; Tobias Philipp; Peter Steinke;
|Term=WS
|Year=2015
|Module=INF-B-270, INF-B-275, INF-LE-EUI, IST-05-PF-HS
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=Klausur
|Description=<center> 
== Die Übung am Montag 6.DS findet ab jetzt immer in APB/E010 statt! ==
 
==Die Übungen am Montag und am Dienstag in der 1.DS fallen aus!==
</center>

 

=Übungen =

Folgende Übungsgruppen finden statt:
* 6. DS Montag APB/E010
* 2. DS Dienstag APB/E001
* 1. DS Mittwoch APB/E001
* 6. DS Mittwoch APB/E009
* 1. DS Donnerstag APB/E008
* 1. DS Freitag WIL/C203
* 2. DS Freitag APB/E008
* 3. DS Freitag APB/E006
* 3. DS Freitag SCH/A252
* 5. DS Freitag APB/E010

== Übungsblätter ==

* [https://ddll.inf.tu-dresden.de/w/images/b/b2/Fs_01.pdf 1.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/d/d5/Fs_02.pdf 2.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/f/fa/Fs_03.pdf 3.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/3/3c/Fs_04.pdf 4.Übungsblatt]

=Vorlesung=

* Die Vorlesung findet montags in der 3. DS in HSZ02 und donnerstags in der 4. DS in HSZ03 statt (ausser zwischen dem 21.12.2015 und dem 03.01.2016)

== Vorlesungsfolien ==

* [https://ddll.inf.tu-dresden.de/w/images/5/5d/FS-2015-einf%C3%BChrung.pdf Einführung]
* [https://ddll.inf.tu-dresden.de/w/images/c/c4/FS-2015-geschichte.pdf Geschichte der Logik]
* [https://ddll.inf.tu-dresden.de/w/images/c/cc/FS-2015-aussagenlogik.pdf Aussagenlogik]

== Weitere Folien ==

* [https://ddll.inf.tu-dresden.de/w/images/0/04/Al_ergaenzung.pdf Aussagenlogik: Ergänzungen 5.11.2015]
* [https://ddll.inf.tu-dresden.de/w/images/8/8d/Beispiel_endlichkeitssatz.pdf Aussagenlogik: Beispiel zum Endlichkeitssatz 5.11.2015]
|Literature=Der erste Teil der Vorlesung basiert auf die folgenden Bücher:

S. Hölldobler: Logik und Logikprogrammierung. Synchron Publishers GmbH, Heidelberg (2009). ISBN 978-3-935025-84-3
[http://www.wv.inf.tu-dresden.de/Teaching/WS-2012/formsys/Korr-Lehrbuch.pdf Korrekturen und Anmerkungen zu diesem Buch]

S. Hölldobler, S. Bader, B. Fronhöfer, U. Hans, P. Hitzler, M. Krötzsch, T. Pietzsch: : Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen; Synchron Publishers GmbH, Heidelberg (2011). ISBN 978-3-935025-85-0
}}

Formale Systeme(WS2015)

2015-11-05T16:40:09Z

Christoph Wernhard:

{{Vorlesung
|Title=Formale Systeme
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler
|Tutors=Emmanuelle Dietz; Tobias Philipp; Peter Steinke;
|Term=WS
|Year=2015
|Module=INF-B-270, INF-B-275, INF-LE-EUI, IST-05-PF-HS
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=Klausur
|Description=<center> 
== Die Übung am Montag 6.DS findet ab jetzt immer in APB/E010 statt! ==
 
==Die Übungen am Montag und am Dienstag in der 1.DS fallen aus!==
</center>

 

=Übungen =

Folgende Übungsgruppen finden statt:
* 6. DS Montag APB/E010
* 2. DS Dienstag APB/E001
* 1. DS Mittwoch APB/E001
* 6. DS Mittwoch APB/E009
* 1. DS Donnerstag APB/E008
* 1. DS Freitag WIL/C203
* 2. DS Freitag APB/E008
* 3. DS Freitag APB/E006
* 3. DS Freitag SCH/A252
* 5. DS Freitag APB/E010

== Übungsblätter ==

* [https://ddll.inf.tu-dresden.de/w/images/b/b2/Fs_01.pdf 1.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/d/d5/Fs_02.pdf 2.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/f/fa/Fs_03.pdf 3.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/3/3c/Fs_04.pdf 4.Übungsblatt]

=Vorlesung=

* Die Vorlesung findet montags in der 3. DS in HSZ02 und donnerstags in der 4. DS in HSZ03 statt (ausser zwischen dem 21.12.2015 und dem 03.01.2016)

== Vorlesungsfolien ==

* [https://ddll.inf.tu-dresden.de/w/images/5/5d/FS-2015-einf%C3%BChrung.pdf Einführung]
* [https://ddll.inf.tu-dresden.de/w/images/c/c4/FS-2015-geschichte.pdf Geschichte der Logik]
* [https://ddll.inf.tu-dresden.de/w/images/c/cc/FS-2015-aussagenlogik.pdf Aussagenlogik]

== Weitere Folien ==

* [https://ddll.inf.tu-dresden.de/w/images/0/04/Al_ergaenzung.pdf Aussagenlogik: Ergänzungen 5.11.2015]
* [https://ddll.inf.tu-dresden.de/w/images/8/8d/Beisp_endlichkeitssatz.pdf Aussagenlogik: Beispiel zum Endlichkeitssatz 5.11.2015]
|Literature=Der erste Teil der Vorlesung basiert auf die folgenden Bücher:

S. Hölldobler: Logik und Logikprogrammierung. Synchron Publishers GmbH, Heidelberg (2009). ISBN 978-3-935025-84-3
[http://www.wv.inf.tu-dresden.de/Teaching/WS-2012/formsys/Korr-Lehrbuch.pdf Korrekturen und Anmerkungen zu diesem Buch]

S. Hölldobler, S. Bader, B. Fronhöfer, U. Hans, P. Hitzler, M. Krötzsch, T. Pietzsch: : Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen; Synchron Publishers GmbH, Heidelberg (2011). ISBN 978-3-935025-85-0
}}

Formale Systeme(WS2015)

2015-11-05T16:37:23Z

Christoph Wernhard:

{{Vorlesung
|Title=Formale Systeme
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler
|Tutors=Emmanuelle Dietz; Tobias Philipp; Peter Steinke;
|Term=WS
|Year=2015
|Module=INF-B-270, INF-B-275, INF-LE-EUI, IST-05-PF-HS
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=Klausur
|Description=<center> 
== Die Übung am Montag 6.DS findet ab jetzt immer in APB/E010 statt! ==
 
==Die Übungen am Montag und am Dienstag in der 1.DS fallen aus!==
</center>

 

=Übungen =

Folgende Übungsgruppen finden statt:
* 6. DS Montag APB/E010
* 2. DS Dienstag APB/E001
* 1. DS Mittwoch APB/E001
* 6. DS Mittwoch APB/E009
* 1. DS Donnerstag APB/E008
* 1. DS Freitag WIL/C203
* 2. DS Freitag APB/E008
* 3. DS Freitag APB/E006
* 3. DS Freitag SCH/A252
* 5. DS Freitag APB/E010

== Übungsblätter ==

* [https://ddll.inf.tu-dresden.de/w/images/b/b2/Fs_01.pdf 1.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/d/d5/Fs_02.pdf 2.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/f/fa/Fs_03.pdf 3.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/3/3c/Fs_04.pdf 4.Übungsblatt]

=Vorlesung=

* Die Vorlesung findet montags in der 3. DS in HSZ02 und donnerstags in der 4. DS in HSZ03 statt (ausser zwischen dem 21.12.2015 und dem 03.01.2016)

== Vorlesungsfolien ==
* [https://ddll.inf.tu-dresden.de/w/images/5/5d/FS-2015-einf%C3%BChrung.pdf Einführung]
* [https://ddll.inf.tu-dresden.de/w/images/c/c4/FS-2015-geschichte.pdf Geschichte der Logik]
* [https://ddll.inf.tu-dresden.de/w/images/c/cc/FS-2015-aussagenlogik.pdf Aussagenlogik]

== Weitere Folien ==

* [https://ddll.inf.tu-dresden.de/w/images/0/04/Al_ergaenzung.pdf Aussagenlogik: Erganzungen 5.11.2015]
|Literature=Der erste Teil der Vorlesung basiert auf die folgenden Bücher:

S. Hölldobler: Logik und Logikprogrammierung. Synchron Publishers GmbH, Heidelberg (2009). ISBN 978-3-935025-84-3
[http://www.wv.inf.tu-dresden.de/Teaching/WS-2012/formsys/Korr-Lehrbuch.pdf Korrekturen und Anmerkungen zu diesem Buch]

S. Hölldobler, S. Bader, B. Fronhöfer, U. Hans, P. Hitzler, M. Krötzsch, T. Pietzsch: : Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen; Synchron Publishers GmbH, Heidelberg (2011). ISBN 978-3-935025-85-0
}}

Formale Systeme(WS2015)

2015-11-05T16:34:54Z

Christoph Wernhard:

{{Vorlesung
|Title=Formale Systeme
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler
|Tutors=Emmanuelle Dietz; Tobias Philipp; Peter Steinke;
|Term=WS
|Year=2015
|Module=INF-B-270, INF-B-275, INF-LE-EUI, IST-05-PF-HS
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=Klausur
|Description=<center> 
== Die Übung am Montag 6.DS findet ab jetzt immer in APB/E010 statt! ==
 
==Die Übungen am Montag und am Dienstag in der 1.DS fallen aus!==
</center>

 

=Übungen =

Folgende Übungsgruppen finden statt:
* 6. DS Montag APB/E010
* 2. DS Dienstag APB/E001
* 1. DS Mittwoch APB/E001
* 6. DS Mittwoch APB/E009
* 1. DS Donnerstag APB/E008
* 1. DS Freitag WIL/C203
* 2. DS Freitag APB/E008
* 3. DS Freitag APB/E006
* 3. DS Freitag SCH/A252
* 5. DS Freitag APB/E010

== Übungsblätter ==

* [https://ddll.inf.tu-dresden.de/w/images/b/b2/Fs_01.pdf 1.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/d/d5/Fs_02.pdf 2.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/f/fa/Fs_03.pdf 3.Übungsblatt]
* [https://ddll.inf.tu-dresden.de/w/images/3/3c/Fs_04.pdf 4.Übungsblatt]

=Vorlesung=

* Die Vorlesung findet montags in der 3. DS in HSZ02 und donnerstags in der 4. DS in HSZ03 statt (ausser zwischen dem 21.12.2015 und dem 03.01.2016)

== Vorlesungsfolien ==
* [https://ddll.inf.tu-dresden.de/w/images/5/5d/FS-2015-einf%C3%BChrung.pdf Einführung]
* [https://ddll.inf.tu-dresden.de/w/images/c/c4/FS-2015-geschichte.pdf Geschichte der Logik]
* [https://ddll.inf.tu-dresden.de/w/images/c/cc/FS-2015-aussagenlogik.pdf Aussagenlogik]

== Weitere Folien ==

|Literature=Der erste Teil der Vorlesung basiert auf die folgenden Bücher:

S. Hölldobler: Logik und Logikprogrammierung. Synchron Publishers GmbH, Heidelberg (2009). ISBN 978-3-935025-84-3
[http://www.wv.inf.tu-dresden.de/Teaching/WS-2012/formsys/Korr-Lehrbuch.pdf Korrekturen und Anmerkungen zu diesem Buch]

S. Hölldobler, S. Bader, B. Fronhöfer, U. Hans, P. Hitzler, M. Krötzsch, T. Pietzsch: : Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen; Synchron Publishers GmbH, Heidelberg (2011). ISBN 978-3-935025-85-0
}}

Techreport3022

2015-08-21T06:34:31Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
|Year=2015
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning
|Archivierungsnummer=15-04
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3023

2015-08-21T06:33:58Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
|Year=2015
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning
|Archivierungsnummer=15-05
}}
{{Publikation Details
|Link=http://cs.christophwernhard.com/papers/behmann.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3022

2015-08-21T06:31:26Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
|Year=2015
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning 15-04
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3022

2015-08-21T06:22:53Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
|Year=2015
|Institution=TU Dresden
|Archivierungsnummer=Knowledge Representation and Reasoning 15-04
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3022

2015-08-21T06:10:33Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
|Year=2015
|Institution=TU Dresden
|Archivierungsnummer=Knowledge Representation and Reasoning 15-04
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Download=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf
|Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3023/en

2015-08-21T06:05:51Z

Christoph Wernhard: Page created automatically by parser function on page Techreport3023

#REDIRECT [[Techreport3023]]

Techreport3023

2015-08-21T06:05:50Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Techreport |Title=Heinrich Behmann's Contributions to Second-Order…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Techreport
|Title=Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
|Year=2015
|Institution=TU Dresden
|Type=Knowledge Representation and Reasoning 15-05
}}
{{Publikation Details
|Link=http://cs.christophwernhard.com/papers/behmann.pdf
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3043

2015-08-21T06:00:35Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications
|To appear=0
|Year=2015
|Booktitle=Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015
|Pages=249-265
|Publisher=Springer
|Editor=Hans de Nivelle
|Series=LLNCS (LNAI)
|Volume=9323
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3043

2015-08-11T19:33:15Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications
|To appear=0
|Year=2015
|Booktitle=Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015
|Publisher=Springer
|Editor=Hans de Nivelle
|Series=LLNCS (LNAI)
|Volume=9323
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Misc3002/en

2015-08-11T13:39:37Z

Christoph Wernhard: Page created automatically by parser function on page Misc3002

#REDIRECT [[Misc3002]]

Misc3002

2015-08-11T13:39:37Z

Christoph Wernhard: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christoph |ErsterAutorNachname=Wernhard }} {{Misc |Title=Some Fragments Towards Establishing Completeness Proper…“

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Misc
|Title=Some Fragments Towards Establishing Completeness Properties of Second-Order Quantifier Elimination Methods
|Year=2015
|Month=August
|Howpublished=Poster presentation at Jahrestreffen der GI Fachgruppe Deduktionssysteme, associated with CADE 25
}}
{{Publikation Details
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Inproceedings3043

2015-08-11T13:26:00Z

Christoph Wernhard:

{{Publikation Erster Autor
|ErsterAutorVorname=Christoph
|ErsterAutorNachname=Wernhard
}}
{{Inproceedings
|Referiert=1
|Title=Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications
|To appear=0
|Year=2015
|Booktitle=Automated Reasoning with Analytic Tableaux and Related Methods: 23rd International Conference, TABLEAUX 2015
|Publisher=Springer
|Editor=Hans de Nivelle
|Series=LLNCS (LNAI)
|Volume=9323
}}
{{Publikation Details
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
|Projekt=SOA-VBQP
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3022/en

2015-08-11T13:25:43Z

Christoph Wernhard: Page created automatically by parser function on page Techreport3022

#REDIRECT [[Techreport3022]]