@string{lipics = "Leibniz International Proceedings in Informatics"}
@string{proc = "Proc.\ "}
@string{lncs = "LNCS"}
@string{lics = "{IEEE} Symposium on Logic in Computer Science"}
@string{cpp = "ACM SIGPLAN International Conference on Certified Programs
 and Proofs"}
@string{tacas = "International Conference on Tools and Algorithms for the
 Construction and Analysis of Systems"}
 
@inbook{KGTM,
author = {Kucherov, Gregory and Tajine, Mohamed},
year = {2006},
month = {01},
pages = {272-286},
title = {Decidability of Regularity and Related Properties of Ground Normal Form Languages},
volume = {118},
isbn = {978-3-540-56393-8},
journal = {Information and Computation},
doi = {10.1007/3-540-56393-8_20}
}

@inproceedings{DT90,
 author    = "Max Dauchet and Sophie Tison",
 title     = "The Theory of Ground Rewrite Systems is Decidable",
 booktitle = proc # "5th " # lics,
 pages     = "242--248",
 year      = 1990,
 doi       = "10.1109/LICS.1990.113750"
}

@article{Collections-AFP,
  author  = {Peter Lammich},
  title   = {Collections Framework},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2009,
  note    = {\url{https://isa-afp.org/entries/Collections.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@inproceedings{LMMF21,
 author    = "Alexander Lochmann and Aart Middeldorp and
              Fabian Mitterwallner and Bertram Felgenhauer",
 title     = "A Verified Decision Procedure for the First-Order Theory of
              Rewriting for Linear Variable-Separated Rewrite Systems
              Variable-Separated Rewrite Systems in {Isabelle/HOL}",
 booktitle = proc # "10th " # cpp,
 editor    = "Cătălin Hriţcu and Andrei Popescu",
 pages     = "250--263",
 year      = 2021,
 doi       = "10.1145/3437992.3439918"
}

@Misc{tata2007,
  author = {H. Comon and M. Dauchet and R. Gilleron and  C. L\"oding
and F. Jacquemard
and D. Lugiez and S. Tison and M. Tommasi},
  title =	 {Tree Automata Techniques and Applications},
  howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
  note = {release October, 12th 2007},
  year =	 2007
}

@inproceedings{MLMF21,
 author    = "Fabian Mitterwallner and Alexander Lochmann and Aart
              Middeldorp and Bertram Felgenhauer",
 title     = "Certifying Proofs in the First-Order Theory of Rewriting",
 editor    = "Jan Friso Groote and Kim G. Larsen",
 booktitle = proc # "27th " # tacas,
 series    = lncs,
 volume    = 12652,
 pages     = "127--144",
 year      = 2021,
 doi       = "10.1007/978-3-030-45237-7\_11"
}

@article{B07,
  author  = {Stefan Berghofer},
  title   = {First-Order Logic According to Fitting},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2007,
  note    = {\url{https://isa-afp.org/entries/FOL-Fitting.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

