id: 05187439
dt: a
an: 05187439
au: Aboul-Hosn, Kamal
ti: A proof-theoretic approach to tactics.
so: Borwein, Jonathan M. (ed.) et al., Mathematical knowledge management. 5th
    international conference, MKM 2006, Wokingham, UK, August 11‒12,
    2006. Proceedings. Berlin: Springer (ISBN 3-540-37104-4/pbk). Lecture
    Notes in Computer Science 4108. Lecture Notes in Artificial
    Intelligence, 54-66 (2006).
py: 2006
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: Zbl 1151.68657
li: doi:10.1007/11812289_6
ab: Summary: Tactics and tacticals, programs that represent and execute several
    steps of deduction, are fundamental to theorem provers providing
    automated tools for creating proofs quickly and easily. The language
    used for tactics is usually a full-scale programming language, separate
    from the language used to represent proofs. Consequently, there is also
    a separation between the use of theorems in proofs and the use of
    tactics. Our goal is to represent tactics in a way that allows them to
    be treated at the same level as proofs and theorems. We also want a
    representation that allows us to formally translate tactics into the
    proof steps they represent. We extend a system presented in [{\it D.
    Kozen} and {\it G. Ramanarayanan}, A proof-theoretic approach to
    knowledge acquisition. Technical report 2005‒1985, Computer Science
    Department: Cornell University (2005); {\it K. Aboul-Hosn} and {\it T.
    D. Andersen}, “A proof-theoretic approach to hierarchical math
    library organization”, Lect.~Notes~Comput.~Sci.~3863, 1‒16 (2006;
    Zbl 1151.68657)] to represent tactics at the same level as theorems and
    move freely from tactics to proof steps and provide an example of its
    usefulness.
rv: