@article{Chaieb_2008,
    doi = {10.1007/s10817-008-9101-x},
    url = {https://doi.org/10.1007%2Fs10817-008-9101-x},
    year = {2008},
    month = {jun},
    publisher = {Springer Science and Business Media {LLC}},
    volume = {41},
    number = {1},
    pages = {33--59},
    author = {Amine Chaieb and Tobias Nipkow},
    title = {Proof Synthesis and Reflection for Linear Arithmetic},
    journal = {Journal of Automated Reasoning}
}

@article{Chaieb_2008, doi = {10.1007/s10817-008-9101-x}, url = {https://doi.org/10.1007%2Fs10817-008-9101-x}, year = {2008}, month = {jun}, publisher = {Springer Science and Business Media {LLC}}, volume = {41}, number = {1}, pages = {33--59}, author = {Amine Chaieb and Tobias Nipkow}, title = {Proof Synthesis and Reflection for Linear Arithmetic}, journal = {Journal of Automated Reasoning} }