Digital Archives and Automated Reasoning Laboratory

The Boolean ring method for propositional theorem proving obtains much attention in recent years. We show in this paper the limitaions of simplification principle in the Boolean ring method by implementing a prover and counting the number of splittings it can help to reduce. Some problems instances, including 3SAT, N-Queen, N-Rook, Pigeonhole, and Ramsey numbers, have been tested on it.
SAT problems on several sets of Boolean ring equations and their complexity classifications are also provided in the discussion section.

The WWW is the most popular system on the Internet, with the user-friendly interface provided by browsers such as Navigator and IE, more and more people are doing their information distribution and acquisition via WWW. However, the rapid growth of the number of homepages on the WWW has made most people lost in the sea of information. Although some search engines provide search services to help users, people using the search services are often disappointed by the large and bad-organized list returned by these search engines.
We propose a personal proxy server in this thesis that not only provides cache mechanism for browsers but also analyzes the user browsing behavior without disturbing the normal browsing activity of the user. The personal proxy server is also the fundamental component of intelligent agent systems and serves as a personal agent. The kept browsing pattern in this personal proxy server can be deemed as user preference that can provide useful assistance for advanced services. Based on the personal proxy, we can develop personal service applications such as personal search engine that satisfies personal information needs. This program is totally written in Java such that it is a platform independent application that can be run anywhere that has a supporting Java virtual machine.

Many methods for finitely representing infinite sequences of terms has been introduced to deal with the divergence of semi-decision processes, like the Knuth-Bendix completion. In this paper, we make a comparison among these classes in their expressive power by verifying their expressive property first in a systematical way - the constructing procedure, for it will be easier and more natural to realize the relations among these classes in this way than in a constructive proof. And, of course, for the reason of correctness, we'll give constructive proofs for the relations we found in this way.

The emerge of the WWW, provides a huge amount of avalable information. Extracting useful information from it could be very useful. However, because of its trememdous size and lacking an universal document structure, this is not an easy task.
In this thesis, we develop a rule-based method to extract information from an HTML file. The method we developed is a way to specify what we want to extract from a document. Given such a rule, the information extracting program can extract information according to that rule, if there is information that fits the specification of the rule.
Based on this information extraction method, we implement two experimental systems to test its usability. They are an instructed spider, and a meta-search engine. An instructed spider can be taught how to traverse, and how to collect. And a meta-search engine posts keyword queries to several search engines and rearrange the responses in a more friendly format.

Computer Viruses have been a major nuisance for computer users for over a decade. The most common techniques for detecting viruses are scan and dynamic trap. To reduce the drawback of the scan tool and the dynamic trap tool, VICE (Virus Instruction Code Emulator) was introduced two years ago. Since the Internet has become widely available, the spread of viruses has become easier than before. In the meantime, it is hard for antivirus software companies to provide effective anti-virus services over the Internet.
In this thesis, we present VICEd (Virus Instruction Code Emulator -- distributed), a generic virus detection mechanism over the Internet. VICEd to build a client/server model, and utilizes the Internet as the communication at both ends of the model. In the second half of the thesis, we present a method for improving the detection ratio of VICE. We propose a new methodology based on fully automatic techniques. We also present a similar method to extract virus behavior rules automatically.

Users will use the on-line manuals proviede by the system while they fall into problem on the UNIX systems. However, the on-line manuals provided by the UNIX system do not improve very much in these years since 1970. They have to be viewed on the text mode page by page and it is inconvinient for most users.
In this paper, we describe how to develop an WWW based manual browsing/indexing system 'ManHunt' that provides Graphics User Interface and hyper-text style manual pages, and natural language full text retrieval.

In this thesis we present an approach to detect viruses and generate virus patterns. Our methodology is a combination of software emulation and knowledge base. It detects viruses based on their behaviour instead of relying on pattern matching. Thus, it is more effective than scan (static or heuristic) against unknown viruses, especially the mutated and polymorphic ones. The emulator emulates the execution in a simulated environment, and the knowledge base provides a way of adding new behaviour patterns. Therefore it is also more flexible than dynamic traps and produces fewer false alarms. In addition to detecting viruses, emulation provides the additional benefit of identifying new virus patterns and cleaning.
One of the biggest advantages of our approach is that emulation can be done on any machines. For example. one can build an emulator for DOS on a workstaion. Then one can use it to determine whether a file contains a PC virus on a workstation. This provides the maximum security agains viruses designed for penetrating anti-virus software, and is ideal for network environments such as the client/server model.

(Abstract is under translation)

The major issue in logics of programs in finding a language appropriate for reasoning about programs. We want a language which has sufficient power to enable programs. The first research devoted to propositional reasoning about programs seems to be that of Fischer and Ladner [1977] on the propositional version of dynamic logic. Dynamic logic applies concepts from modal logic to a relational semantics of programs to yield various systems for reasoning about the before-after behavior of programs. When we run a program, only one statement is excecute at any given time. We may know that the original language has no the expressive power for processes executing concurrently. In the following, we add some new operations into the propositional dynamic logic to describe naturally the behavior of the execution about concurrent processes but we do not enlarge the expressive power of PDL.