Digital Archives and Automated Reasoning Laboratory

Department of Computer Science and Information Engineering

National Taiwan University

[ 聯絡方式 ]

● 數位典藏與自動推論實驗室

國立臺灣大學資訊工程學系 lab303

TEL:02-33664888#303

thdl.contact@lab303.csie.ntu.edu.tw

臺灣大學數位人文研究中心(Research Center for Digital Humanity)

[ 招生資訊 ]

請直接連絡老師信箱:hsiang(at)csie.ntu.edu.tw

2014 lab303 招生資訊

實驗室氣氛良好、學長姐都很和善,有興趣的話隨時歡迎到德田館lab303找大家輕鬆聊聊天。


本實驗室的主要研究領域為自動推論與數位典藏,近期則重心則轉移到數位人文的研究。自動推論的目的是發展可自動化的邏輯系統,以能利用計算機證明數學定理,乃至自動回答問題;數位典藏則利用運用資訊科技將文化資產保存,數位人文則希望結合資訊技術與數位典藏的資源,提供人文研究一個全新的視野。

這是一個需要結合不同工具與取徑的目標,所涉及的資訊領域包括Data Mining、Visualization、Database Systems、Information Retrieval、GIS(geographic Information System)、電子書等等,我們因此歡迎具備跨領域能力與創意的研究者,如果你對人文研究也有些好奇或興趣,更歡迎加入我們的團隊。


[ 實驗室及相關機構簡介 ]

● 數位典藏與自動推論實驗室

本實驗室自1993年項潔教授自美返台任教時成立,主要研究領域為自動推論與數位典藏,近期則重心則轉移到數位人文的研究。自動推論的目的是發展可自動化的邏輯系統,以能利用計算機證明數學定理,乃至自動回答問題;數位典藏則利用運用資訊科技將文化資產保存,數位人文則希望結合資訊技術與數位典藏的資源,提供人文研究一個全新的視野。

項潔教授自台大數學系畢業,美國伊利諾大學香檳分校(University of Illinois at Urbana-Champaign)電腦科學博士。此後他任教於紐約大學石溪分校(SUNY at Stony Brook),並於該校取得正教授資格。項潔教授有超過150篇的專書、期刊及會議論文,曾擔任數種國際期刊的編輯(editorial boards)。他也曾任教於法國巴黎大學、Nancy大學、Orleans大學的客座教授,義大利米蘭大學的約聘教授,在法國資訊暨自動化研究院(INRIA)及法國國家科學院(CNRS)及日本新世代電腦中心(ICOT)擔任過客座研究員。項教授也曾獲得兩次國科會傑出研究獎、教育部大專教師產學合作研發績效卓越獎。目前他擔任台灣大學資訊工程系暨資訊網路與多媒體研究所特聘教授,中央研究院資訊科學所合聘研究員,並兼任台灣大學數位典藏研究發展中心與出版中心主任。

● 台大數位人文研究中心

http://www.digital.ntu.edu.tw

數位人文研究中心(以下稱數位人文中心)是與本實驗室合作最密切的一個校內單位。數位人文中心結合了校內跨領域研究發展團隊,持續數位化保存臺灣具重要性、唯一性、即時性、脆弱性的珍品。除典藏珍貴的文化資產外,更致力於打造完整的數位研究環境,期待透過數位的力量,將文化資產轉化為研究素材,進而發展數位人文研究。

數典中心目前已建置十餘個資料庫,共累計132萬餘筆詮釋資料(metadata)、207萬餘筆影像、1億6千餘萬字全文,內容涵括明清檔案、臺灣古契書、日治時期法院檔案與統計資料、國民黨黨史、臺灣省諮議會檔案、黨外雜誌及社運剪報、老照片等,呈現臺灣豐富的文化遺產與多元的歷史觀點。

數典中心的目標除了保存史料外,也希望藉由資訊科技,節省研究花費的大量時間與人力,使研究者跨越時空限制,在短時間找到所需資料。而資料庫累積的大量資料,更能使研究者在搜尋與比對間,延伸發現新的研究議題與知識,從而擴展研究視野,探索人文研究的新領域。資訊科技的應用在於突破人力不及之處,由量的累積帶來質的轉變,提供資料之間各種關連性,協助研究者闡發問題意識,探問人文研究新的方法論。

此外,本中心期望成為一個交流對話的場域,不定期舉辦工作坊、研討會、讀書會、訪問獎助計畫等,邀請資訊人文各界的研究者投入,反饋具體的批評建議,加強數位典藏與人文研究的連結。

● Term rewriting systems

這方面最重要的成果有兩項。第一項為發現一個基於Boolean ring的canonical term rewriting system for Boolean algebra,並用以將term rewriting提升到first order的自動推論上。項教授關於這個結果的論文發表在Journal of Artificial Intelligence上,並於1993年被該期刊選為被引用最多50篇論文之一。

另一個成果是解決了term rewriting裡面一個重要問題:Knuth-Bendix Completion Procedure的abnormal termination問題。這個結果使得Knuth-Bendix Completion對eqational logic是完備的。這個方法幾乎已經變成所有現代的equational theorem provers的基本reasoning engine。

項教授因為在term rewriting system領域中的成就,1998年被聯合國教科文組織(UNESCO)委託成立有關在term rewriting的工作小組,收要的成員都是該領域的資深專家,被委託規劃更屬殊榮。項教授更擔任此工作小組的主席至2001年。

● Proof methods & automated deduction

這方面最成果亦有兩項。第一項是發現transfinite semantic trees的證明方法,並基於這個方法設計了ordered resolution及證明其完備性。這個結果證明了open 19年的Wos-Robinson Conjecture,而ordered resolution更成為resolution theorem proving中最被普遍使用的方法。另一項成果是proof orderings。這個嶄新的proof theory以成為教科書的教材,並在2006年獲得IEEE LICS的Test-of-time Award。

用推理方法解決數學的open problems

自動推論研究除了方法的完備性外,更需能用所設計的理論解決實際問題。為了達到後者,也需要在search的方法上有所突破。本實驗是在search的strategies上有深入的研究,並將之實現於theorem provers中,並以證明了數十個有限數學裡的open problems,如算出25 Queen問題的解有2,207,893,435,808,352個,

● 數位典藏

項教授於1996年起開始投入數位典藏與數位圖書館的工作,從一開始的台大電子圖書館/博物館計畫、國科會數位博物館計畫到數位典藏國家型科技計畫,十年年推動了國內數位典藏工作與研究,使數位典藏在台灣從無到有,至今日的蓬勃發展。

項教授在2002年接任台灣大學圖書館館長,除了將台大典藏的文化資產數位化外,也盡力收集散佚民間的重要史料,並有系統的數位化。

台灣歷史數位圖書館與歷史資訊學

近年來台大圖書館與本實驗室的合作,在文建會支持下,有系統的蒐集重要的台灣史第一手史料,進行數位化全文建檔與人工標點著錄,包括了明清台灣行政檔案、淡新檔案、岸裡大社文書、古文書、地方志、札記等等。全文已經超過8,000萬字,加上其他整理取得的全文資料,總計超過一億五千萬自,應掌握超過80%之所有明清時期台灣史的第一手資料。這些資料已經建置成「台灣歷史數位圖書館」,提供全文檢索,是全世界獨一無二的台灣史全文資料庫。除了第一手史料外,我們也著手建立各種研究所需要的參考工具,如年表、中西曆轉換、人名地名辭典、官職表等等。

這個資料庫除了強調全文資料量的豐富外,更重要的是在設計上強調文史研究者需求。我們將檢索看成使用的最基本(而非最重要)的功能,強調檢索所得資料的後分類,及相關文件的連結關係。

我們所蒐集的歷史全文資料,其隱含的資訊量與知識量是極驚人的。我們相信,隨著量變而來的,將是研究上得「質變」。換句話說,隨著如此大量且易於使用的全文資料,歷史研究的方式亦應該隨之改變。而資訊科技將在這個新的研究方法論上,扮演極為重要和關鍵的角色。我們將此稱為「歷史資訊學」或「數位人文學」,這也是本實驗室以後研究的主要方法。

● 其他相關連結

國立台灣大學圖書館

Metacat (跨越台灣各大學圖書館搜索書籍)

杜博士的blog