|
|
|
|
|
|
Help | Seminars List | Add Seminar | Edit Seminars | Tips for organisers | RSS | ics Calendar | Search | Send comments about this website to seminar-master@cecs.anu.edu.au
Contact: Michelle.Moravec@anu.edu.au CS PHD MONITORING
Mechanizing Properties of CFGs in HOLMs Aditi Barthwal (School of Computer Science, CECS)DATE: 2009-09-24 TIME: 13:00:00 - 13:30:00 LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU ABSTRACT: I will present the formalization of various properties of Context-Free grammars in the HOL theorem prover. Among the important properties proven, I will present the results for pumping lemma for CFGs, the property that pushdown automata are equivalent to context-free grammars and the equivalence of acceptance by the two possible criteria for pushdown automata. These are acceptance by empty stack and acceptance by final state. The two are not equivalent for the deterministic pushdown automaton although they are for the non-deterministic pushdown automaton.
|