Attribut:Long description DE
Aus International Center for Computational Logic
Dies ist eine Eigenschaft des Typs Zeichenkette.
C
Coprocessor ist ein eigenständiges Werkzeug zur Formelvereinfachung für verschiedenen Probleme. Die meisten Techniken wurden für CNF Formeln entwickelt, die Optimierungsvariante MaxSAT wird aber ebenso unterstützt wie MUS. Ein Teil der Techniken kann auch für QBF verwendet werden. Coprocessor implementiert beinah alle veröffentlichten Vereinfachungstechniken. Zu den Vereinfachungen können Statistiken ausgegeben werden, außerdem kann die Reihenfolge der Techniken angegeben werden, und Variablen können von der Vereinfachung ausgeschlossen werden. Dadurch kann Coprocessor auch Formeln vereinfachen, für die nachher mehrere Modelle auf einer Untermenge ihrer Variablen generiert werden soll. +
N
''Nemo'' ist ein freies System zum schnellen und skalierbaren logischen Schließen mit Datalog-artigen Regeln. Es ist verfügbar als Kommandozeilen-Tool <tt>nmo</tt>, durch Anbindungen an verschiedene Programmiersprachen und als [https://tools.iccl.inf.tu-dresden.de/nemo/ online verfügbare Browser-Anwendung].
Kernziele von Nemo sind Performance, Deklarativität, Vielseitigkeit und Verlässlichkeit. Nemo ist in Rust implementiert. Sein Datenmodell vereint Kompatibilität mit Standardformaten wie [https://www.w3.org/TR/rdf11-concepts/ RDF] und [https://www.w3.org/TR/sparql11-overview/ SPARQL] mit bewährten Konventionen und Features der Logikprogrammierung.
Die von Nemo unterstützte Regelsprache ist eine Erweiterung von Datalog, welche unter anderem die folgenden Features unterstützt:
* Datentypen mit dazugehörigen Prädikaten und Funktionen (z.B. arithmetische Vergleiche und Operationen).
* Existenzielle Regeln (auch bekannt als ''Tuple-Generating Dependencies'')
* Stratifizierte Negation
Einsatzgebiete von Nemo umfassen ''Datenanalyse'', ''Anfragebeantwortung'', ''Datenintegration'' sowie spezielle Aufgaben wie ''Programmanalyse'' und ''ontologisches Schließen''. Es erlaubt dabei die gleichzeitige Verwendung mehrerer Datenquellen in diversen Formaten (RDF-Graphen, CSV-Dateien, usw.).
Nemo ist ein Nachfolgeprojekt von [[VLog]] und verwendet einige von dessen Technologien (insbesondere vertikale Speicherstrukturen – ''column stores''), hat aber gleichzeitig eine völlig neue Architektur und Implementierung, welche Nemo die Unterstützung zusätzlicher Features bei gleichzeitig höherer Performance erlaubt. +
R
Riss ist ein SAT Solver (Softwarepaket), welches auf MiniSat 2.2 und Glucose 2.2 basiert, und welches the conflict driven clause learning Algorithmus verwended. Riss beherbergt außerdem den Formelvereinfacher Coprocessor, der Formeln vor, und während, der Suche bearbeiten kann. Riss schließt viele Suchalgorithmuserweiterungen ein, und enthält im Moment (2014) circa 500 Parameter. Während der Suche kann Riss einen Unerfüllbarkeitsbeweis im DRAT-Format generieren, sodass sowohl Antworten für erfüllbare, als auch für unerfüllbare Probleme überprüft werden können. Diese Beweise können auch schon während der Suche überprüft werden.
Das Softwarepaket enthält außerdem ein Werkzeug, welches Features der CNF-Formel extrahieren kann, sodass zusammen mit einem Machine-Learning Werkzeug eine Konfiguration für Riss basierend auf der gegebenen Formel ausgewählt werden kann. Weiterhin ist der paralleler Portfolio-Solver Priss enthalten, welcher auch Unerfüllbarkeitsbeweise während der parallelen Suche ausgeben kann, wobei geteilte Klauseln berücksichtigt werden.
Ein weitere paralleler Lösungsansatz ist enthalten, Iterative Partitioning. Das dazugehörige System pcasso lässt nicht mehrere Solver auf der Formel laufen, sondern unterteilt den Suchraum des Problems in Partitionen, und weist anschließend jeder Partition einen sequentiellen Solver zu. Zusätzlich wird die originale Formel gelöst. Wenn weitere Resourcen zur Verfügung stehen, werden die Partitinoen ihrerseite wieder unterteilt und parallel zu den anderen Partitionen gelöst. Pcasso kann außerdem gelernte Klauseln teilen. Formelvereinfachung während der Suche werden im Moment nicht unterstützt. +
S
Semantic MediaWiki (SMW) ist eine freie Erweiterung von MediaWiki – dem Wiki-System auf dem auch Wikipedia aufbaut – mit der die Inhalte eines Wikis durchsucht, organisiert, gebrowst, ausgewertet und mit anderen geteilt werden können. Während traditionelle Wikis nur Texte enthalten, die Computer weder verstehen noch auswerten können, fügt SMW semantische Annotationen hinzu, die das Wiki in eine gemeinschaftlich verwaltete Datenbank verwandeln.
Seit seinem ersten Release in 2005 hat Semantic MediaWiki zu einem überaus erfolgreichen Open-Source-Projekt entwickelt, das auf hunderten Websites weltweit eingesetzt wird – darunter auch die des International Center for Computational Logic. Darüberhinaus entstanden eine große Zahl an Erweiterungen, die SMW um Möglichkeiten der Bearbeitung, Darstellung und Erkundung von Daten erweitern. Der Begriff "Semantic MediaWiki" wird in diesem Zusammenhang oft für diese gesamte Familie von Softwareprodukten verwendet. +
V
'''A current successor system of VLog is [[Nemo]], which improves upon the methods and features of VLog in several ways.'''
<b>VLog</b> (Vertical Datalog) is a <b>rule engine</b> that supports reasoning over <i>Horn existential rules</i> with stratified negation and, implicitly, <i>Datalog</i>. It uses a novel strategy based on a vertical storage architecture [1], which exhibits a state-of-the-art performance, distinguishing itself by excellent memory footprint and scalability [2].
The engine applies a bottom-up strategy for existential rules, supporting the two most studied materialisation algorithms: the <i>Skolem</i> and the <i>Restricted (Standard) Chase</i>. The latter is recommended for use, as it leads to termination in more cases.
VLog can be used for <i>query answering</i>, <i>federated reasoning</i> and <i>data integration</i>. It allows the use of multiple datasources at the same time, of various types (RDF stores, CSV files, OWL ontologies and remote SPARQL endpoints).
VLog is open-source, and it provides two main tools for such reasoning tasks:
* the core C++ reasoner <b>VLog</b> (https://github.com/karmaresearch/vlog), which is a command-line client with an interactive web interface that provides graphical representations of each rule executions, useful for tracing and debugging rule programs. The pre-compiled binaries can be obtained via Docker (karmaresearch/vlog), which facilitates a platfom-independent use.
* the Java API <b>Rulewerk</b> (https://github.com/knowsys/rulewerk), which integrates the core reasoner for all major OSs, allowing an easy embedding into other applications, and providing additional functionality. It comprises of multiple <i>Maven</i> modules (<i>org.semanticweb.rulewerk</i>): <i>rulewerk-core</i> provides essential data models for rules and facts, and an interface for essential reasoner functionality; <i>rulewerk-parser</i> supports processing knowledge bases in Rulewerk syntax; <i>rulewerk-owlapi</i> supports converting rules from OWL ontology using the OWL API; <i>rulewerk-rdf</i> supports loading data from RDF files; <i>rulewerk-graal</i> supports converting rules, facts and queries from Graal API objects and DLGP files; <i>rulewerk-client</i> is stand-alone application that builds a command-line client for Rulewerk; <i>rulewerk-commands</i> provides support for running commands, as done by the client; <i>rulewerk-vlog</i> supports using VLog as a reasoning backend for Rulewerk; and <i>rulewerk-examples</i> demonstrates the use of above functionality.
[1] Urbani, J., Jacobs, C., Krötzsch, M.: Column-oriented Datalog materialization for large
knowledge graphs. In: Proc. 30th AAAI Conf. on Artificial Intelligence (AAAI’16). pp.
258–264. AAAI Press (2016)
[2] Urbani, J., Krötzsch, M., Jacobs, C., Dragoste, I., Carral, D.: Efficient model construction
for Horn logic with VLog: System description. In: Proc. 9th Int. Joint Conf. on Automated
Reasoning (IJCAR’18). LNAI, Springer (2018)
W
Dieser frei verfügbare Datensatz beinhaltet anonymisierte Logs mehrerer hundert Millionen '''SPARQL-Anfragen aus dem Wikidata SPARQL Webservice''', die im Zusammenhang mit der folgendne Publikation gesammelt worden sind:
<div class="card"><div class="card-body">Stanislav Malyshev, Markus Krötzsch, Larry González, Julius Gonsior, Adrian Bielefeldt:<br/>
'''[[Inproceedings3044|Getting the Most out of Wikidata: Semantic Technology Usage in Wikipedia’s Knowledge Graph]].'''<br/> In Proceedings of the 17th International Semantic Web Conference (ISWC-18), Springer 2018. [https://iccl.inf.tu-dresden.de/w/images/5/5a/Malyshev-et-al-Wikidata-SPARQL-ISWC-2018.pdf PDF]</div></div>
Weitere Veröffentlichungen zu diesen Daten sind im Abschnitt ''Publikationen'' zu finden.
Die Daten beinhalten neben den Anfragen auch genaue Zeitstempel und grobe Informationen zu den Anfragequellen (''user agents''). Links zu allen Datensätzen und Details zu deren Inhalt und Erstellung finden sich auf der [[Wikidata SPARQL Logs/en|englischsprachigen Seite]]. +
a
Abstract Dialectical Frameworks (ADF) sind eine Generalisierung von Dung Argumentation Frameworks.
“Abstract Dialectical Frameworks solved by Binary Decision Diagrams, developed in Dresden” ( ADF -BDD) ist ein neuer Ansatz, welcher die Akzeptanzfunktionen eines ADF als reduziert geordnete binäre Entscheidungsdiagramme (reduced ordered binary decision diagrams - roBDD) übersetzt.
Das tool basiert auf dem Konzept, dass einige - sonst schwer zu lösende - Entscheidungsprobleme bei der Berechnung der ADF-Semantiken in polynomieller Zeit von roBDDs gelöst werden können.
Aktuelle state-of-the-art solver basieren derzeit auf SAT oder Antwortmengenprogrammierung basierten ansätzen, weshalb adf-bdd ein Alleinstellungsmerkmal besitzt.
ADF-BDD ist in RUST geschrieben, welches gute Performanz und einen hohen Grad an Speicher- sowie Typ-sicherheit bietet.
Zudem bietet der rust-compiler hochgradig optimierten Maschinencode, während der Techstack simple bleibt. +
