@article{DieterMartaguetWolf2008, author = {Dieter, Anne and Martaguet, Laurent and Wolf, Catherine}, title = {Simone de Beauvoir zum 100. Geburtstag}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-16582}, year = {2008}, abstract = {Im Januar 2008 w{\"a}re Simone de Beauvoir, die wohl bedeutendste und gleichermaßen umstrittenste franz{\"o}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{\"u}ter. Das traf auch auf ihre gelebte Rebellion f{\"u}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.}, language = {de} } @masterthesis{Repp2023, type = {Bachelor Thesis}, author = {Repp, Leo}, title = {Extending the automatic theorem prover nanoCoP with arithmetic procedures}, doi = {10.25932/publishup-57619}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-576195}, school = {Universit{\"a}t Potsdam}, pages = {52}, year = {2023}, abstract = {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{\"a}ngerprojekte leanCoP, nanoCoP und leanCoP-Ω vor, auf dessen Vorlage nanoCoP-Ω entwickelt wurde. Es folgt eine ausf{\"u}hrliche Erkl{\"a}rung der Konzepte, um welche der nicht-klausale Konnektionskalk{\"u}l erweitert werden muss, um eine Behandlung von arithmetischen Ausdr{\"u}cken und Gleichheiten in den Kalk{\"u}l zu integrieren, sowie eine Beschreibung der Implementierung dieser Konzepte in nanoCoP-Ω. Als letztes folgt eine experimentelle Evaluation von nanoCoP-Ω. Es wurde ein ausf{\"u}hrlicher Vergleich von Laufzeit und Anzahl gel{\"o}ster Probleme im Vergleich zum {\"a}hnlich aufgebauten Theorembeweiser leanCoP-Ω auf Basis der TPTP-Benchmark durchgef{\"u}hrt. Ich komme zu dem Ergebnis, dass nanoCoP-Ω deutlich schneller ist als leanCoP-Ω ist, jedoch weniger gut geeignet f{\"u}r gr{\"o}ßere Probleme. Zudem konnte ich feststellen, dass nanoCoP-Ω falsche Beweise liefern kann. Ich bespreche, wie dieses Problem gel{\"o}st werden kann, sowie einige m{\"o}gliche Optimierungen und Erweiterungen des Beweissystems.}, language = {en} }