Proceedings:
Book One
Volume
Issue:
Proceedings of the AAAI Conference on Artificial Intelligence, 6
Track:
Automated Reasoning
Downloads:
Abstract:
The WATSON automatic programming system computes formal behavior specifications for process-control software from informal "scenarios": traces of typical system operation. It first generalizes scenarios into stimulus-response rules, then modifies and augments these rules to repair inconsistency and incompleteness. It finally produces a formal specification for the class of computations which implement that scenario and which are also compatible with a set of "domain axioms". A particular automaton from that class is constructed as an executable prototype for the specification. WATSON’s inference engine combines theorem proving in a very weak temporal logic with faster and stronger, but approximate, model-based reasoning. The use of models and of closed-world reasoning over "snapshots" of an evolving knowledge base leads to an interesting special case of non-monotonic reasoning.
AAAI
Proceedings of the AAAI Conference on Artificial Intelligence, 6