RnDCircle Logo
권기항 연구실
동아대학교 컴퓨터공학과 권기항 교수
Computability Logic
Proof Theory
Logic Programming
연구 영역
기본 정보
논문·특허
과제
구성원

권기항 연구실

동아대학교 컴퓨터공학과 권기항 교수

권기항 연구실은 computability logic 및 proof theory 관점에서 알고리즘의 명세와 실행 의미를 연구합니다. 논리프로그래밍에서 cut predicate를 choice-disjunctive goal로 고수준화하고, 시퀀트 기반 휴리스틱 proof procedure를 통해 first-order logic과 propositional logic의 proof search를 제어하는 기법을 개발합니다. 또한 CoLweb을 중심으로 logical pseudocode와 imperative code를 연결하고, dynamic programming에서 forward chaining과 automatic memoization이 되도록 언어 의미를 설계합니다. 모듈 언어에서는 qualified names를 제거하는 module weakening 방식을 제안합니다.

Computability LogicProof TheoryLogic ProgrammingSequent CalculusDynamic Programming
대표 연구 분야
연구 영역 전체보기
논리계산에서 cut의 고수준화와 휴리스틱 proof search thumbnail
논리계산에서 cut의 고수준화와 휴리스틱 proof search
High-level Treatment of Cut and Heuristic Proof Search in Logic Computation
연구 분야 상세보기
연구 성과 추이
표시된 성과는 수집된 데이터 기준으로 산출되며, 일부 차이가 있을 수 있습니다.
주요 논문
5
논문 전체보기
1
Article
|
인용수 0
·
2026
Algorithm Specification in CoLweb with Imperative Code
Keehang Kwon, Seongjoon Kwon
https://doi.org/10.13140/rg.2.2.21111.07841
Code (set theory)
Formal specification
Source code
Software
Key (lock)
2
Article
|
인용수 0
·
2026
Implementing Computability Logic CL3
Keehang Kwon, Seongjoon Kwon
https://doi.org/10.13140/rg.2.2.31775.83363
3
Preprint
|
인용수 0
·
2023
Implementing Dynamic Programming in Computability Logic Web
Keehang Kwon
arXiv (Cornell University)
본 연구에서는 CoLweb이라 불리는 알고리즘 언어에 해당하는, 새로운 알고리즘의 정의를 제시한다. CoLweb[1]의 장점은 알고리즘 설계를 매우 유연하게 만든다는 데 있다. 즉, 비분산 컴퓨팅과 분산 컴퓨팅 모두에 대해 알고리즘 설계를 고수준의 증명-수반(proof-carrying), 분산형(distributed-style) 접근으로 강제한다. 우리는 이러한 접근이 알고리즘 설계를 단순화한다고 주장한다. 또한 재귀적 논리/함수형 알고리즘, 명령형 알고리즘, 객체지향 명령형 알고리즘, 신경망(neural-nets), 인터랙션 넷(interaction nets), 증명-수반 코드(proof-carrying code) 등 다른 접근들을 통합한다. 응용의 한 예로, 우리는 혼 절(Horn clause) 정의를 두 종류로 정교화한다: 맹목적 전칭-양화(blind-universally-quantified, BUQ) 정의와 병렬 전칭-양화(parallel-universally-quantified, PUQ) 정의이다. BUQ 정의는 지식기반이 확장되지 않으며 그 증명 절차가 역방향 체이닝(backward chaining)에 기반하는 Prolog에서의 전통적 정의에 해당한다. 반면 PUQ 정의에서는 지식기반이 되고, 그 증명 절차가 순방향 체이닝(forward chaining)과 { it automatic memoization}을 도출한다.
http://arxiv.org/abs/2304.01539
Computer science
Prolog
Memoization
Programming language
Forward chaining
Theoretical computer science
Functional programming
Chaining
Haskell
Computability
최신 정부 과제
1
과제 전체보기
1
2011년 5월-2012년 5월
|61,510,000
치매 및 중증환자를 위한 대소변 자동 알람 모니터링 시스템
본 과제는 간병인이 대소변 관련 업무를 수동으로 수행하는 문제를 줄이기 위해, 환자의 활동성을 보장하면서 자동으로 상태를 판단하는 시스템을 개발하는 연구임. 연구목표는 무선 통신 환경에서 모듈화 구성과 데이터베이스 기반 환자관리를 제공하며 환자와 간병인, 사회에 도움이 되는 시스템 구현임. 핵심 연구내용은 검교정된 상대습도 계측기 오차 ±2%℃ 이내 성능, Zigbee 무선 통신, 독립 전원으로 14시간 이상 동작, 대소변 정확 판단 및 기저귀 교체시기 판단, 데이터베이스화하여 착용자 정보 관리임. 기대효과는 수동 업무 자동 대체로 간병 효율 증대, 고령인구 수요 충족, 대형병원·요양원 적용 및 사회적 비용 절감, 청결상태 유지와 건강상태 변화 파악 가능함.
치매
중환자
대변
소변
알람 모니터링 시스템