Logic Programming and the Specification of Circuits
The work
| Authors | W. F. Clocksin |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1985 |
| Citekey | clocksin1985logic |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-72 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| DOI | 10.48456/tr-72 |
|---|---|
| report_number | UCAM-CL-TR-72 |
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-72.html |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | camilleri1986hardware |
| Distinct from | camilleri1988simulation |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985why |
| Distinct from | hunt1994fm8501 |
| Distinct from | leeser1988reasoning |
| Distinct from | melham1987abstraction |
| Distinct from | winskel1987relating |
From bibtex.
Abstract
Logic programming (see Kowalski, 1979) can be used for specification and automatic reasoning about electrical circuits. Although Propositional Logic has long been used for describing the truth functions of combinational circuits, the more powerful Predicate Calculus on which logic programming is based has seen relatively little use in design automation. Previous researchers have introduced a number of techniques similar to logic programming, but many of the useful consequences of the logic programming methodology have not been exploited. This paper first reviews and compares three methods for representing circuits, which will be called here the functional method, the extensional method, and the definitional method. The latter method, which conveniently admits arbitrary sequential circuits, is then treated in detail. Some useful consequences of using this method for writing directly executable specifications of circuits are described. These include the use of quantified variables, verification of hypothetical states, and sequential simulation.
A copy is held
pdf, 620.3 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 23:53 UTC |
| Approved by | a person 2026-09-23 14:10 UTC |
Filed under
Cite it as
@techreport{clocksin1985logic,
title = {Logic Programming and the Specification of Circuits},
author = {W. F. Clocksin},
year = {1985},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
doi = {10.48456/tr-72},
}
This record lives at https://refs.drheap.org/clocksin1985logic/ and will keep doing so.