5 ( & ( 1 = - (
52&=1,.,),/2=2),&=1(
7RP/;,9QXPHU±
0(72'$7$%/,&2:$$3235$:12ĝû52=802:$ē
7RPDV]-$508ĩ(.Formalizacja metod tablicowych dla logik zda i logik nazw 7RUXĔ :\GDZQLFWZR 1DXNRZH 80. VV ,6%1
0HWRGD EDGDZF]D VWDQRZL MHGHQ ] SRGVWDZRZ\FK SU]HGPLRWyZ ILOR]RILF]QHM UH
IOHNVMLGRW\F]ąFHMQDXNL:V]F]HJyOQRĞFLS\WDQLHRPHWRGĊGRW\F]\QDXNIRUPDOQ\FK
NWyUHVDPHZSHZQ\P]DNUHVLHVWDQRZLąPHWRGĊGODQDXNSU]\URGQLF]\FKGRVWDUF]D
MąFLPQDU]ĊG]LGRRSLVXLDQDOL]\]MDZLVNHPSLU\F]Q\FK
=NROHLS\WDQLHRPHWRGĊQDXNIRUPDOQ\FK]DZLHUDZVRELHS\WDQLHRV]HURNR±QD
JUXQFLHDQDOL]\LNU\W\NLPHWRGEDGDZF]\FK±G\VNXWRZDQH]DJDGQLHQLHPHWRG\SR
SUDZQHJRZ\FLąJDQLDZQLRVNyZ]GDQ\FKSU]HVáDQHN=DJDGQLHQLHWRVWDQRZLSU]\NáDG
OLF]Q\FK SU]\SDGNyZ QLHSXVWHJR SU]HNURMX SyO ]DLQWHUHVRZDĔ ILOR]RILL RUD] ORJLNL
0RQRJUDILDFormalizacja metod tablicowych dla logik zda i logik nazw -$508ĩ(.
MDNRSUDFD]]DNUHVXORJLNLWUDNWXMHZáDĞQLHRMHGQHM]ZLHOXPHWRGZHU\ILNDFML
SRSUDZQRĞFLUR]XPRZDĔZSLVXMąFVLĊZWHQVSRVyEZ]DNUHVNU\W\NLPHWRGEDGDZ
F]\FKRUD]ILOR]RILL
&HO NVLąĪNL PRĪQD ODSLGDUQLH RNUHĞOLü SU]H] MHM W\WXá ± MDNR IRUPDOL]DFMĊ PHWRG
WDEOLFRZ\FKGODORJLN]GDĔRUD]ORJLNQD]Z1LH]QDF]\WRMHGQDNĪHFHOHPPDE\ü
Z\F]HUSDQLHPRĪOLZ\FKRSLVyZPHWRG\WDEOLFRZHMGODWHJRF]\LQQHJRV\VWHPXORJL
NL]GDĔRUD]ORJLNLQD]Z$XWRUSRGNUHĞODĪH
=DPLDVW>«@RSLV\ZDüNROHMQHV\VWHP\WDEOLFRZHGODWHMVDPHMORJLNLZ\]QDF]RQHMVHPDQ
W\F]QLH VSUyEXMHP\ V]XNDü ZVSyOQ\FK FHFK V\VWHPyZ WDEOLFRZ\FK GOD UyĪQ\FK ORJLN Z\
]QDF]RQ\FKVHPDQW\F]QLH -$508ĩ(.
: NVLąĪFH GąĪ\ VLĊ ]DWHP GR SRGDQLD PHWDORJLF]QHJR RSLVX V\VWHPyZ WDEOL
FRZ\FKZRJyOH
-HGQą]ZDĪQLHMV]\FKSUDFQDWHPDWPHWRG\WDEOLFRZHMMHVWPRQRJUDILDHandbook of tableau methods '¶$*267,12*$%%$<+$(+1/(326(**$ NWyUHMQDMQRZV]HZ\GDQLHXND]DáRVLĊ
Z U
'2, KWWS G[GRLRUJ UI
5(&(1=-(
3U]H]PHWRG\WDEOLFRZHDXWRUUR]XPLHMDNWRRNUHĞODZHZVWĊSLHVSRVyEGHILQLR
ZDQLDV\VWHPyZWDEOLFRZ\FKRUD]SRMĊüSR]ZDODMąF\FKXG]LHOLüRGSRZLHG]LQDS\WD
QLH F]\ ZV\VWHPDFK W\FK ]DFKRG]L UHODFMD Z\QLNDQLD ORJLF]QHJR GOD GDQHM SDU\
XSRU]ąGNRZDQHM ]ELRUXIRUPXá SU]HVáDQHN LIRUPXá\ ZQLRVNX 3UH]HQWDFMDSRGHM
ĞFLDGRPHWRG\WDEOLFRZHMSU]HGVWDZLRQHMZPRQRJUDILLUR]SRF]\QDVLĊRG]GHILQLR
ZDQLD ORJLNL RG VWURQ\ VHPDQW\F]QHM F]\OL RG VWURQ\ UHODFML Z\QLNDQLD ORJLF]QHJR
NRQVHNZHQFML VHPDQW\F]QHM GOD NWyUHM V\VWHP WDEOLFRZ\ MHVW EXGRZDQ\ 2JyOQLH
U]HF] XMPXMąF V\VWHP WDEOLFRZ\ SRZLQLHQ E\ü VNRQVWUXRZDQ\ Z WDNL VSRVyE DE\
UHODFMDGRZLHGOQRĞFL NRQNUHWQLHMUHODFMDNRQVHNZHQFMLJDáĊ]LRZHM Z\]QDF]RQDSU]H]
WHQ V\VWHP E\áD UyZQD UHODFML Z\QLNDQLD ORJLNL GOD NWyUHM V\VWHP WHQ ]RVWDá ]EX
GRZDQ\,QQ\PLVáRZ\ GREU]H]GHILQLRZDQ\V\VWHPWDEOLFRZ\PDE\üSHáQ\L]JRGQ\
Z]JOĊGHPZ\MĞFLRZHMVHPDQW\NL3U]H]SHáQRĞüDXWRUUR]XPLH]DZLHUDQLHVLĊUHODFML
NRQVHNZHQFML VHPDQW\F]QHM Z UHODFML NRQVHNZHQFML JDáĊ]LRZHM 1DWRPLDVW SU]H]
]JRGQRĞü±]DZLHUDQLHVLĊUHODFMLJDáĊ]LRZHMZUHODFMLNRQVHNZHQFMLVHPDQW\F]QHM
2F]\ZLĞFLH XMĊFLH WDEOLFRZH QDOHĪ\ WUDNWRZDü MDNR XMĊFLH V\QWDNW\F]QH $XWRU
VWZLHUG]DĪH
PHWRGĊWDEOLFRZąWUDNWXMHP\LGHILQLXMHP\ZNVLąĪFHZVSRVyEF]\VWRV\QWDNW\F]Q\W]QMDNR
PHWRGĊSU]HNV]WDáFDQLDQDSLVyZGDQHJRMĊ]\NDZFHOXX]\VNDQLDRGSRZLHG]LQDS\WDQLHF]\
UR]SDWU\ZDQHZQLRVNRZDQLHMHVWSRSUDZQH -$508ĩ(.
6WDQGDUGRZ\P XMĊFLHP V\QWDNW\F]Q\P MHVW SRGHMĞFLH DNVMRPDW\F]QH : SUDF\
]HVWDZLDVLĊ]DOHW\RUD]ZDG\RE\GZXSRGHMĞü$XWRU]DXZDĪDĪHPHWRGDWDEOLFRZD
MHVWEDUG]LHMDWUDNF\MQDRGSRGHMĞFLDDNVMRPDW\F]QHJRZDVSHNFLHEXGRZ\GRZRGyZ
,VWRWQLH PHWRGD DNVMRPDW\F]QD Z\PDJD QLHPDáHM SRP\VáRZRĞFL ZSU]\SDGNX NRQ
VWUXRZDQLDGRZRGXGDQHMIRUPXá\QDJUXQFLHMDNLHJRĞ ]ELRUXIRUPXáàDWZR]ZHU\
ILNRZDüZUDPDFKV\VWHPXDNVMRPDW\F]QHJRF]\SRGDQ\GRZyGMHVWSRSUDZQ\1LH
LVWQLHMHMHGQDNHIHNW\ZQDPHWRGDNWyUDRSLV\ZDáDE\MDNLFKSRGVWDZLHĔRUD]RGHUZDĔ
QDOHĪ\GRNRQDüDE\QDJUXQFLHSU]HVáDQHNRUD]DNVMRPDWyZGRZLHĞüRGSRZLHGQLHJR
ZQLRVNX0HWRGDWDEOLFRZDQDWRPLDVWZZLĊNV]RĞFLSU]\SDGNyZXPRĪOLZLDSU]HSUR
ZDG]DQLHGRZRGXZVSRVyE]DXWRPDW\]RZDQ\F]\WHĪ]DOJRU\WPL]RZDQ\WR]QDF]\
GRZRG]ąFĪH]GDQHJR]ELRUXSU]HVáDQHNPRĪQDSRSUDZQLHZ\SURZDG]LüGDQ\ZQLR
VHN SRVWĊSXMHP\ ]JRGQLH ]SHZQ\PL UHJXáDPL F]\ WHĪ ZVND]DQLDPL PyZLąF\PL
RW\P MDN QDOHĪ\ SURZDG]Lü GRZyG WDEOLFRZ\ 1LHZąWSOLZLH MHGQDN V\VWHP\ DNVMR
PDW\F]QH Vą SURVWV]H GR ]GHILQLRZDQLD ± FKRü SRGDQLH DGHNZDWQHM DNVMRPDW\NL MHVW
]Z\NOH WUXGQH 3UDZGą MHVW ĪH XMĊFLH DNVMRPDW\F]QH SRVLDGD ]DOHW\ NWyU\FK EUDN
PHWRG]LHWDEOLFRZHMWDGUXJDMHGQDNMHVW]GHF\GRZDQLHEDUG]LHMDWUDNF\MQDZ]DNUH
VLHNRQVWUXNFMLGRZRGX
1DVWĊSXMąFHSRMĊFLDVWDQRZLąRĞWHRULLPHWRG\WDEOLFRZHM UHJXáDWDEOLFRZDJDáąĨ
RUD]WDEOLFD$XWRUSUH]HQWXMHLFKRJyOQHRUD]F]\VWRIRUPDOQHXMĊFLH]DSRPRFąSRMĊü
WHRULRPQRJRĞFLRZ\FK 2JyOQLH Z FHOX SRGDQLD ĞFLVáHJR RSLVX PHWRG\ WDEOLFRZHM
DXWRUZSURZDG]DGHILQLFMHQDVWĊSXMąF\FKSRMĊü
5(&(1=-(
D UHJXáDWDEOLFRZD
E JDáąĨ
◆JDáąĨPDNV\PDOQD
◆JDáąĨ]DPNQLĊWD RWZDUWD
◆UHODFMDNRQVHNZHQFMLJDáĊ]LRZHM
F WDEOLFD
◆WDEOLFDNRPSOHWQD
◆WDEOLFD]DPNQLĊWD RWZDUWD
SU]\F]\PRNUHĞODMąFSRMĊFLHJDáĊ]LNRU]\VWD]SRMĊFLDUHJXá\WDEOLFRZHMZGHILQLFML
WDEOLF\ ]DĞ RGZRáXMH VLĊ GR SRMĊFLD JDáĊ]L : PRQRJUDILL QLH ZSURZDG]D VLĊ SRMĊü
]EĊGQ\FK
$XWRUSUH]HQWXMH]DVWRVRZDQLDVZRMHMWHRULLQDSU]\NáDG]LHPRGDOQHMORJLNLQD]Z
SU]\ WDN ]ZDQHM LQWHUSUHWDFML de re =RVWDMą WDNĪH ]DSUH]HQWRZDQH ]DVWRVRZDQLD QD
JUXQFLH WHRULL NRQVWUXNFML V\VWHPyZ WDEOLFRZ\FK GOD ORJLN PRGDOQ\FK ]VHPDQW\Ną
PRĪOLZ\FKĞZLDWyZRUD]RSLVXSU]HMĞFLDRGDEVWUDNF\MQLHUR]XPLDQHMZSUDF\JDáĊ]L
LWDEOLF\ GR LQWXLF\MQHJR VWDQGDUGRZHJR SRMĊFLD JDáĊ]L RUD] WDEOLF\ 3RGREQLH MDN
0HOYLQ )LWWLQJ ),77,1* DXWRU WZLHUG]L ĪH XMĊFLH VWDQGDUGRZH VWDQRZL ]D
VWRVRZDQLHSRGHMĞFLDEDUG]LHMDEVWUDNF\MQHJRNWyUH]RVWDáR]DSUH]HQWRZDQHZPRQR
JUDILL1DOHĪ\]DXZDĪ\üĪHVWDQGDUGRZDPHWRGDMHVWQLH]Z\NOHáDWZDZ]DVWRVRZD
QLX 1LHVWHW\ ZLąĪH VLĊ ] SRZDĪQ\PL WUXGQRĞFLDPL PHWDORJLF]Q\PL NWyU\FK QLH
SRGREQDXVXQąüSU]\SR]LRPLH]áRĪRQRĞFLMĊ]\NDSRGHMĞFLDVWDQGDUGRZHJR
3UDFD QLH SRUXV]D GZyFK DVSHNWyZ %DGDQLD Z QLHM ]DZDUWH Vą ]DZĊĪRQH GR ]D
NUHVXORJLN]GDĔRUD]ORJLNQD]ZFRZ\NOXF]DORJLNL]NZDQW\ILNDWRUDPLDZV]F]H
JyOQRĞFL.ODV\F]Qą/RJLNĊ3UHG\NDWyZ'UXJLPRF]HNLZDQ\PUR]V]HU]HQLHP]DNUHVX
EDGDĔSRZLQQRE\üGRSXV]F]HQLHZLHORZDUWRĞFLRZRĞFLORJLN5R]ZLą]DQLHW\FKSUR
EOHPyZVWDQRZLáRE\QDWXUDOQąNRQW\QXDFMĊUR]ZDĪDĔSU]HGVWDZLRQ\FKSU]H]DXWRUD
=ZáDV]F]D UR]V]HU]HQLH WHRULL WDEOLF QD ORJLNL ] NZDQW\ILNDWRUDPL E\áRE\ SRĪąGDQH
]WHM UDFML ĪH PLHOLE\ĞP\ WDEOLFRZą PHWDWHRULĊ REHMPXMąFą FDáą ORJLNĊ NODV\F]Qą
DZLĊFSRGVWDZ\PHWRGRORJLF]QHQDXNL3RQLHZDĪMHGQDNNVLąĪNDMHVWGRĞüREV]HUQD
MDN QD SUDFĊ ] ORJLNL ZLĊF ]DZĊĪHQLH SROD EDGDZF]HJR GR GREU]H ]GHILQLRZDQHJR
]DNUHVXMHVWZSHáQLDNFHSWRZDOQHLVWDQRZLSXQNWZ\MĞFLDGRGDOV]\FKXRJyOQLHĔ
.VLąĪND SRGDMH EDUG]R RJyOQą PHWRGĊ NRQVWUXRZDQLD SHáQ\FK L ]JRGQ\FK V\VWH
PyZWDEOLFRZ\FKNWyUHSR]ZDODMąVSUDZG]DüSRSUDZQRĞüUR]XPRZDĔZ\VWĊSXMąF\FK
ZKXPDQLVW\FH L LQQ\FK G\VF\SOLQDFK RUD] HNVSOLNRZDü ORJLF]QH ]DáRĪHQLD NWyUH
ZW\FK UR]XPRZDQLDFK Z\VWĊSXMą 5HDVXPXMąF PRĪHP\ SRGDü QDVWĊSXMąFH ]DOHW\
QRZDWRUVNLHJR RSLVX PHWRG\ WDEOLFRZHM NWyU\ ]RVWDá ]DSUH]HQWRZDQ\ ZUHFHQ]RZD
QHMNVLąĪFH
◆ 3UHF\]DFMDSRGHMĞFLDVWDQGDUGRZHJR±UR]ZLą]DQLHSHZQ\FKSUREOHPyZSRMD
ZLDMąF\FKVLĊQDSR]LRPLHLQWXLF\MQ\P
7HJRURG]DMXSRGHMĞFLH]RVWDáR]DSUH]HQWRZDQHPLĊG]\LQQ\PLZ35,(67
5(&(1=-(
◆ 0RĪOLZRĞüRNUHĞOHQLDSRSUDZQHJRSU]HMĞFLDRGXMĊFLDDEVWUDNF\MQHJRGRVWDQ
GDUGRZHJR
◆ 0RĪOLZRĞüEDGDQLDUHODFMLSRPLĊG]\UyĪQ\PLV\VWHPDPLWDEOLFRZ\PL
◆ 8MĊFLHPHWRG\WDEOLFRZHMZRJyOH QDJUXQFLHORJLN]GDQLRZ\FKLORJLNQD]Z
DQLHW\ONRZRGQLHVLHQLXGRGDQHJRV\VWHPXORJLNL
◆ 0RĪOLZRĞü Z\ND]DQLD SHáQRĞFL L ]JRGQRĞFL V\VWHPX WDEOLFRZHJR Z]JOĊGHP
GDQHJRV\VWHPXORJLNL
◆ 2SLVRJyOQ\FKZDUXQNyZSRSUDZQHJREXGRZDQLDV\VWHPyZWDEOLFRZ\FK
2SLVDQH ]DOHW\ ZDUWR E\áRE\ XGRVWĊSQLü V]HUV]HM SXEOLF]QRĞFL SRSU]H] DQJOR
MĊ]\F]QąSXEOLNDFMĊ]DZLHUDMąFąSRMĊFLDWHMWDEOLFRZHMPHWDWHRULL
/,7(5$785$
'¶$*267,120DUFHOOR'RY0*$%%$<5HLQHU+ b+1/(-RDFKLP326(**$ UHG Hand- book of tableau methods'RUGUHFKW±%RVWRQ±/RQGRQ .OXZHU$FDGHPLF3XEOLVKHU.
),77,1* 0HOYLQ First-order logic and automated theorem proving 1HZ <RUN 6SULQJHU
9HUODJ
-$508ĩ(. 7RPDV] Formalizacja metod tablicowych dla logik zda i logik nazw 7RUXĔ
:\GDZQLFWZR80.
35,(67*UDKDPAnintroduction to non-classical logic. From if to is&DPEULGJH 8QLYHUVLW\
3UHVV
Mateusz Klonowski doktorant na Wydziale Humanistycznym Uniwersytetu Mikoaja Kopernika w Toruniu
