TY - THES A1 - Repp, Leo T1 - Extending the automatic theorem prover nanoCoP with arithmetic procedures T1 - Erweiterung des automatischen Theorembeweisers nanoCoP um Arithmetik und Gleichheit behandelnde Verfahren N2 - In dieser Bachelorarbeit implementiere ich den automatischen Theorembeweiser nanoCoP-Ω. Es handelt sich bei diesem neuen System um das Ergebnis einer Portierung von Arithmetik-behandelnden Prozeduren aus dem automatischen Theorembeweiser mit Arithmetik leanCoP-Ω in das System nanoCoP 2.0. Dazu wird zuerst der mathematische Hintergrund zu automatischen Theorembeweisern und Arithmetik gegeben. Ich stelle die Vorgängerprojekte leanCoP, nanoCoP und leanCoP-Ω vor, auf dessen Vorlage nanoCoP-Ω entwickelt wurde. Es folgt eine ausführliche Erklärung der Konzepte, um welche der nicht-klausale Konnektionskalkül erweitert werden muss, um eine Behandlung von arithmetischen Ausdrücken und Gleichheiten in den Kalkül zu integrieren, sowie eine Beschreibung der Implementierung dieser Konzepte in nanoCoP-Ω. Als letztes folgt eine experimentelle Evaluation von nanoCoP-Ω. Es wurde ein ausführlicher Vergleich von Laufzeit und Anzahl gelöster Probleme im Vergleich zum ähnlich aufgebauten Theorembeweiser leanCoP-Ω auf Basis der TPTP-Benchmark durchgeführt. Ich komme zu dem Ergebnis, dass nanoCoP-Ω deutlich schneller ist als leanCoP-Ω ist, jedoch weniger gut geeignet für größere Probleme. Zudem konnte ich feststellen, dass nanoCoP-Ω falsche Beweise liefern kann. Ich bespreche, wie dieses Problem gelöst werden kann, sowie einige mögliche Optimierungen und Erweiterungen des Beweissystems. N2 - In this bachelor’s thesis I implement the automatic theorem prover nanoCoP-Ω. This system is the result of porting arithmetic and equality handling procedures first introduced in the automatic theorem prover with arithmetic leanCoP-Ω into the similar system nanoCoP 2.0. To understand these procedures, I first introduce the mathematical background to both automatic theorem proving and arithmetic expressions. I present the predecessor projects leanCoP, nanoCoP and leanCoP-Ω, out of which nanCoP-Ω was developed. This is followed by an extensive description of the concepts the non-clausal connection calculus needed to be extended by, to allow for proving arithmetic expressions and equalities, as well as of their implementation into nanoCoP-Ω. An extensive comparison between both the runtimes and the number of solved problems of the systems nanoCoP-Ω and leanCoP-Ω was made. I come to the conclusion, that nanoCoP-Ω is considerably faster than leanCoP-Ω for small problems, though less well suited for larger problems. Additionally, I was able to construct a non-theorem that nanoCoP-Ω generates a false proof for. I discuss how this pressing issue could be resolved, as well as some possible optimizations and expansions of the system. KW - automatic theorem prover KW - leanCoP KW - connection calculus KW - tptp KW - arithmetic procedures KW - equality KW - omega KW - arithmethische Prozeduren KW - automatisierter Theorembeweiser KW - Konnektionskalkül KW - Gleichheit KW - leanCoP KW - Omega KW - TPTP Y1 - 2023 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-576195 ER - TY - JOUR A1 - Dieter, Anne A1 - Martaguet, Laurent A1 - Wolf, Catherine T1 - Simone de Beauvoir zum 100. Geburtstag BT - eine biographische Skizze aus menschenrechtlicher Perspektive N2 - Im Januar 2008 wäre Simone de Beauvoir, die wohl bedeutendste und gleichermaßen umstrittenste französische Schriftstellerin und Philosophin des 20. Jahrhunderts, einhundert Jahre alt geworden. Ihre wissenschaftlichen wie literarischen Arbeiten waren getragen vom Geist der Freiheit und Gleichheit aller Individuen. Besonders Beauvoirs tiefgreifende Analyse der geschlechtlichen Rollenverteilung in der Gesellschaft und ihre radikale Forderung nach Gleichstellung der Geschlechter bewegten zutiefst die Gemüter. Das traf auch auf ihre gelebte Rebellion für weibliche Autonomie als Part der Selbstbestimmung der Menschen zu. Der Beitrag begibt sich anhand des von Simone de Beauvoir selbst gezeichneten Entwicklungsweges auf Spurensuche nach Besonderheiten, die sie zu diesen tiefgreifenden emanzipatorischen Vorstellungen ebenso wie zu ihrem weltweiten politischen Engagement veranlassten. KW - Menschenrechte KW - Freiheit KW - Gleichheit KW - Gleichberechtigung von Mann und Frau KW - Empowerment KW - Geschichte KW - Biographie Y1 - 2008 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-16582 ER -