Zobrazeno 1 - 10
of 89
pro vyhledávání: '"Kwon, Keehang"'
Autor:
Kwon, Keehang
We present a novel definition of an algorithm and its corresponding algorithm language called CoLweb. The merit of CoLweb [1] is that it makes algorithm design so versatile. That is, it forces us to a high-level, proof-carrying, distributed-style app
Externí odkaz:
http://arxiv.org/abs/2304.01539
Autor:
Kwon, Keehang, Kang, Daeseong
Although the notion of qualified names is popular in module systems, it causes severe complications. In this paper, we propose an alternative to qualified names. The key idea is to import the declarations in other modules to the current module before
Externí odkaz:
http://arxiv.org/abs/2210.03413
Autor:
Kwon, Keehang
Inspired by computability logic\cite{Jap03}, we refine recursive function definitions into two kinds: blindly-quantified (BQ) ones and parallel universally quantified (PUQ) ones. BQ definitions corresponds to the traditional ones where recursive defi
Externí odkaz:
http://arxiv.org/abs/2207.12137
Autor:
Kwon, Keehang
Theorem proving is one of the oldest applications which require heuristics to prune the search space. Invertible proof procedures has been the major tool. In this paper, we present a novel and powerful heuristic called $nongshim$ which can be seen as
Externí odkaz:
http://arxiv.org/abs/2202.10639
Autor:
Kwon, Keehang, Kwon, Hyung Joon
Proofs (sequent calculus, natural deduction) and imperative algorithms (pseudocodes) are two well-known coexisting concepts. Then what is their relationship? Our answer is that \[ imperative\ algorithms\ =\ proofs\ with\ cuts \] This observation lead
Externí odkaz:
http://arxiv.org/abs/2201.12572
Autor:
Kwon, Keehang
Although algorithm is one of the central subjects, there have been little common understandings of what an algorithm is. For example, Gurevich view algorithms as abstract state machines, while others view algorithms as recursors. We promote a third v
Externí odkaz:
http://arxiv.org/abs/2108.10728
Autor:
Kwon, Keehang
{\em Computability logic} (CoL) is a powerful, mathematically rigorous computational model. In this paper, we show that CoL-web, a web extension to CoL, naturally supports web programming where database updates are involved. To be specific, we discus
Externí odkaz:
http://arxiv.org/abs/2101.09222
Autor:
Kwon, Keehang
Computability logic(CoL) is a powerful computational model. In this paper, we show that CoL naturally supports multi-agent programming models where resources (coffee for example) are involved. To be specific, we discuss an implementation of the Starb
Externí odkaz:
http://arxiv.org/abs/2010.08925
Autor:
Kwon, Keehang, Kang, Daeseong
We discuss an agent-based approach to proof design and implementation, which we call {\it Lemma Flow Diagram} (LFD). This approach is based on the multicut rule with $shared$ cuts. This approach is modular and easy to use, read and automate. Thus, we
Externí odkaz:
http://arxiv.org/abs/2002.00666
Autor:
Kwon, Keehang
{\em Computability logic} (CoL) is a powerful computational model which views computational problems as games played by a machine and its environment. In this paper, we show that CoL naturally supports multiagent programming models with distributed c
Externí odkaz:
http://arxiv.org/abs/1909.07036