TY - GEN
T1 - Reasoning about computations using two-levels of logic
AU - Miller, Dale
PY - 2010/1/1
Y1 - 2010/1/1
N2 - We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state theorems about computational specifications. This logic is classical or intuitionistic and should contain strong proof principles such as induction and co-induction. The second level of logic, called the "specification logic", is used to specify computation. While computation can be specified using a number of formal techniques - e.g., Petri nets, process calculus, and state machines - we shall illustrate the merits and challenges of using logic programming-like specifications of computation.
AB - We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state theorems about computational specifications. This logic is classical or intuitionistic and should contain strong proof principles such as induction and co-induction. The second level of logic, called the "specification logic", is used to specify computation. While computation can be specified using a number of formal techniques - e.g., Petri nets, process calculus, and state machines - we shall illustrate the merits and challenges of using logic programming-like specifications of computation.
U2 - 10.1007/978-3-642-17164-2_4
DO - 10.1007/978-3-642-17164-2_4
M3 - Conference contribution
AN - SCOPUS:78650738860
SN - 364217163X
SN - 9783642171635
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 34
EP - 46
BT - Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings
PB - Springer Verlag
ER -