Cyber & formal methods publications

We present a new approach for symbolic evaluation that can efficiently compute these conditions by binding variables to conditional values and avoiding the path feasibility analysis of traditional symbolic evaluation.

We use a combination of techniques to automatically generate new instructions and new compact encodings for virtual instructions.

In this paper, we present a Java-enabled application with a multimodal (pen and voice) interface over the web. Our implementation approach was to add Java to the set of languages…

We describe an extension of Earley's parser for stochastic context-free grammars that computes quantities given a stochastic context-free grammar and an input string.

We propose a snake-based approach that lets a user specify only the distant endpoints of the curve he wishes to delineate without having to supply an almost complete polygonal approximation.

MGTPs have solved previously open problems in finite algebra, produced rapid proofs of condensed detachment problems, and are providing an inferential infrastructure for knowledge-processing research at ICOT. This paper describes…

In this paper we report on work done to modify a model elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of…

In this paper we report on a resolution proof method for logics of belief that is suitable for automatic reasoning in commonsense domains.

We propose a method of nonmonotonic reasoning in which the notion of inference from specific bodies of evidence plays a fundamental role. The formalization is based on autoepistemic logic, but…

Starting with a causal theory, explanations can be generated either by abductive reasoning, or by adding closure axioms and minimizing causation within a deductive framework. The latter method is strictly…

This paper makes "reversibility" explicit and demonstrates by means of examples from Tunica and Klamath that two-level phonology does have certain desirable capabilities that are not found in grammars of…

This paper describes a new Prolog-based implementation of PTTP. It uses three compile-time transformations to translate formulas into Prolog clauses that directly execute, with the support of a few run-time…