Please use this identifier to cite or link to this item: https://hdl.handle.net/10593/24268
Title: Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
Other Titles: Canonical and Dual Erotetic Calculi for First-Order Logic
Authors: Chlebowski, Szymon
Advisor: Wiśniewski, Andrzej. Promotor
Keywords: teoria dowodu
inferencyjna logika pytań
logika I-rzędu
proof theory
inferential erotetic logic
first-order logic
Issue Date: 2018
Abstract: W swojej książce First-Order Logic and Automated Theorem Proving Fitting wprowadził pojęcie własności niesprzeczności (CP), blisko spokrewnione z pojęciem zbioru Hintikki. Własność niesprzeczności jest rodziną formuł spełniającą pewne kryteria. Główne twierdzenie dotyczące CP głosi, że każdy zbiór należący do CP posiada model Herbranda. Z punktu widzenia teorii dowodu, własności niesprzeczności mogą zostać z powodzeniem użyte w celu jednorodnego dowodu pełności dla rozmaitych systemów dowodzenia twierdzeń, w tym tabel analitycznych, systemów aksjomatycznych, rachunku sekwentów czy rezolucji, nie mogą być jednak w prosty sposób wykorzystane w dowodach pełności systemów dualnych, np. dualnej rezolucji. W rozprawie wprowadzone zostają pojęcia dualnego zbioru Hintikki oraz własności falsyfikowalności (RF) oraz udowodnione zostaje twierdzenie o istnieniu kontrmodelu, zgodnie z którym każdy zbiór należący do RF posiada kontrmodel Herbranda. Wprowadzona zostaje technika oparta na pojęciu RF, którą zastosowano w celu uzyskania jednorodnego dowodu pełności dla trzech dualnych rachunków erotetycznych dla logiki I-rzędu zdefiniowanych w rozprawie.
In his book First-Order Logic and Automated Theorem Proving Fitting introduced the notion of a first-order consistency property, which is closely related to the notion of a Hintikka set. Consistency property is a family of sets of first-order sentences meeting certain conditions. The central observation called model existence theorem states that every member of a consistency property has a Herbrand model. From a proof-theoretical point of view, the notion of a consistency property enables an uniform completeness proof for various proof systems such as tableaux method, sequent calculus, and resolution, but is not so natural when applied to dual systems, such as dual resolution. In the dissertation notions of dual Hintikka set and first-order refutability property are introduced together with counter model existence theorem, which states that every member of a first-order refutability property can be falsified in some Herbrand model. These concepts are used to prove completeness of three new dual erotetic calculi (based on Inferential Erotetic Logic and resolution) for first-order logic.
Description: Wydział Nauk Społecznych
URI: http://hdl.handle.net/10593/24268
Appears in Collections:Doktoraty (WNS)
Doktoraty 2010-2022 /dostęp ograniczony, możliwy z komputerów w Bibliotece Uniwersyteckiej/

Files in This Item:
File Description SizeFormat 
main.pdf
  Restricted Access
606.21 kBAdobe PDFView/Open
Show full item record



Items in AMUR are protected by copyright, with all rights reserved, unless otherwise indicated.