My academic interests are logical calculi, proof theory, mathematical logic, complexity theory, automata, combinatorics, and the philosophy of mathematics. My PhD thesis is about sequent calculi for first-order logics with free variables.

The focus of my research has been a method called *variable splitting*. This is a method applicable to free-variable tableaux, free-variable sequent calculi, connection methods, and matrix characterizations, that reduces redundancies in the search space by exploiting a relationship between branching formulas and universal formulas. Using contextual information to differentiate between occurrences of free variables, the method can be used to assigne different values to these occurrences in a consistent way. Read more in my PhD Thesis.

Journal of Symbolic Computation, volume 47, number 9, pages 1046–1065, Springer-Verlag, 2012. [Show BibTeX code]

@article{HansenAntonsenGieseWaaler12, author = {Christian Mahesh Hansen and Roger Antonsen Martin Giese and Arild Waaler}, title = {Incremental {V}ariable {S}plitting}, journal = {Journal of {S}ymbolic {C}omputation}, volume = 47, number = 9, pages = {1046–1065}, year = 2012, publisher = {Springer-Verlag}, ee = {http://dx.doi.org/10.1016/j.jsc.2011.12.032} }

PhD Thesis, Department of Informatics, University of Oslo, 2008. [Show BibTeX code]

@PhdThesis{Antonsen08, author = {Roger Antonsen}, title = {The {M}ethod of {V}ariable {S}plitting}, school = {University of Oslo}, year = 2008, key = {Automated Reasoning, Logic, Proof Theory, Connection Method, Tableau Calculus}, address = {Department of Informatics}, month = {June} }

In Nicola Olivetti and Camilla Schwind, editors, TABLEAUX '07, Automated Reasoning with Analytic Tableaux and Related Methods, Position Papers, LSIS.RR.2007.002, 2007. [Show BibTeX code]

@InProceedings{HansenAntonsenWaaler07, author = {Christian Mahesh Hansen and Roger Antonsen and Arild Waaler}, title = {Incremental {C}losure of {V}ariable {S}plitting {T}ableaux}, year = 2007, booktitle = {TABLEAUX '07, Automated Reasoning with Analytic Tableaux and Related Methods, Position Papers}, editor = {Nicola Olivetti and Camilla Schwind}, pages = {65–78}, publisher = {LSIS}, volume = {LSIS.RR.2007.002} }

In Frank Pfenning, editor, CADE-21, 21th International Conference on Automated Deduction, Bremen, Germany, volume 4603, pages 132–146, Lecture Notes in Computer Science, Springer-Verlag, 2007. [Show BibTeX code]

@InProceedings{AntonsenWaaler07b, author = {Roger Antonsen and Arild Waaler}, editor = {Frank Pfenning}, title = {A {L}abelled {S}ystem for {IPL} with {V}ariable {S}plitting}, booktitle = {CADE-21, 21th International Conference on Automated Deduction, Bremen, Germany}, volume = 4603, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, year = {2007}, isbn = {978-3-540-73594-6}, pages = {132–146}, ee = {http://dx.doi.org/10.1007/978-3-540-73595-3_10} }

Journal of Automated Reasoning, volume 38(1–3), pages 3–30, 2007. [Show BibTeX code]

@ARTICLE{AntonsenWaaler07, author = {Roger Antonsen and Arild Waaler}, title = {Liberalized {V}ariable {S}plitting}, journal = {Journal of Automated Reasoning}, year = {2007}, number = {1–3}, volume = 38, ee = {http://dx.doi.org/10.1007/s10817-006-9055-9}, pages = {3–30} }

In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX, Koblenz, Germany, volume 3702 of Lecture Notes in Computer Science, pages 33-47, Springer-Verlag, 2005. [Show BibTeX code]

@InProceedings{AntonsenWaaler05, author = {Roger Antonsen and Arild Waaler}, title = {Consistency of {V}ariable {S}plitting in {F}ree {V}ariable {S}ystems of {F}irst-{O}rder {L}ogic}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX, Koblenz, Germany}, year = 2005, pages = {33–47}, series = {Lecture Notes in Computer Science}, editor = {Bernhard Beckert}, volume = 3702, isbn = {3-540-28931-3}, publisher = {Springer-Verlag}, ee = {http://dx.doi.org/10.1007/11554554_5} }

In Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, 04 July – 08 July, 2004, volume 106, pages 1–5, CEUR Workshop Proceedings, 2004. [Show BibTeX code]

@InProceedings{Antonsen04, author = {Roger Antonsen}, title = {Uniform {V}ariable {S}plitting}, year = 2004, booktitle = {Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, 04 July – 08 July, 2004}, volume = 106, publisher = CEUR Workshop Proceedings}, pages = {1–5}, issn = {1613–0073}, ee = {http://ceur-ws.org/Vol-106/01-antonsen.pdf} }

In Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX, Rome, Italy, Lecture Notes in Computer Science, volume 2796, pages 214–229, Springer-Verlag, 2003. [Show BibTeX code]

@InProceedings{WaalerAntonsen03, author = {Arild Waaler and Roger Antonsen}, title = {A {F}ree {V}ariable {S}equent {C}alculus with {U}niform {V}ariable {S}plitting}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX, Rome, Italy}, year = 2003, pages = {214–229}, series = {Lecture Notes in Computer Science}, number = 2796, publisher = {Springer-Verlag}, ee = {http://dx.doi.org/10.1007/978-3-540-45206-5_17} }

Master Thesis, Language, Logic and Information, Department of Linguistics, University of Oslo, 2003. [Show BibTeX code]

@mastersthesis{Antonsen03, author = {Roger Antonsen}, title = {Free {V}ariable {S}equent {C}alculi}, year = 2003, month = {May}, address = {Language, Logic and Information, Department of Linguistics}, school = {University of Oslo}, publisher = {University of Oslo} }

*Some talks related to research.*