Grŵp Ymchwil Cyfrifiadureg Damcaniaethol

Cynhadledd Parhad, Cymharedd, Adeiladwaith yn Faro.

Ulrich ac Olga wedi mynychu cyfarfod prosiect CID blynyddol ac yn mynd i roi sgyrsiau yn y gynhadledd Parhad, Cymharedd, Adeiladwaith yn Faro.

Ymwelodd Monika, Olga ac Ulrich â UC fel rhan o brosiect CORCON yr UE

Monika, Olga ac Ulrich wedi ymweld â UC fel rhan o brosiect CORCON yr UE yn Ebrill 2017

Trosolwg o'r Grŵp

Mae'r 'Grŵp Theori' yn gwneud ymchwil mewn ystod eang o bynciau mewn Cyfrifiadureg Damcaniaethol.

Beth yw Cyfrifiadureg Damcaniaethol?

Mae Cyfrifiadureg Damcaniaethol (TCS) yn defnyddio dulliau mathemategol a rhesymegol i ddeall natur cyfrifiant ac i ddatrys problemau sylfaenol sy'n codi trwy ddefnydd ymarferol beunyddiol o systemau cyfrifiadurol.

Mae llawer o lwyddiant TCS yn ddyledus i Alan Turing (1912-1954), y mae llawer yn ei ystyried yn dad i TCS, ac i Kurt Gödel (1906-1978), sylfaenydd rhesymeg fodern. Rhoddodd Turing ddiffiniad manwl gywir o'r syniad o gyfrifiannu trwy ei beiriannau Turing a dangosodd fod yna broblemau cyfrifiadurol na fydd unrhyw gyfrifiadur, pa mor bwerus bynnag, byth yn gallu eu datrys. Dangosodd Gödel y gellir ffurfioli a mecaneiddio ymresymu rhesymegol yn llawn, ond ar y llaw arall, mae llawer o briodweddau strwythurau data a systemau cyfrifiadurol yn eu hanfod yn amhendant, nad yw'n brofadwy nac yn wrthbrofadwy.

Yn seiliedig ar fewnwelediadau sylfaenol Turing a Gödel, a ddangosodd bŵer a chyfyngiadau cyfrifiant a rhesymeg, datblygodd TCS amrywiaeth eang o ddulliau i brofi cywirdeb system gyfrifiadurol ac i ddarganfod gwallau meddalwedd cyn iddynt arwain at fethiannau cyfrifiadurol trychinebus. Mae TCS hefyd yn asesu anhawster cynhenid problemau cyfrifiadurol, yn datblygu dulliau newydd effeithlon i ddatrys problemau cyfrifiadurol caled ac yn darparu methodolegau pwerus ar gyfer datblygu meddalwedd cywir a dibynadwy.

Mae prif bynciau TCS yn cynnwys Theori Algorithmau, Strwythurau Data, Theori Cyfrifiadura, Cymhlethdod Cyfrifiadurol, Modelau Cyfrifiant, er enghraifft Cyfochrog, Dosranedig, Cydamserol, Tebygol, a Chyfrifiant Cwantwm, Theori Automata ac Ieithoedd Ffurfiol, Damcaniaeth Gwybodaeth, Rhesymeg mewn Cyfrifiaduron Gwyddoniaeth.

Mae Grŵp Theori Abertawe yn enwog yn rhyngwladol am ei ymchwil mewn Rhesymeg mewn Cyfrifiadureg. Mae meysydd ymchwil gweithredol yn cynnwys: Damcaniaeth Gyfrifiadurol, Cymhlethdod Cyfrifiadurol, Theori Prawf, Theori Math, Theori Gêm, Cydredeg, Deallusrwydd Artiffisial (Datrys Boddhad, Systemau Aml-asiant, Damcaniaeth Dadl, Dysgu Peiriannau, AI a'r Gyfraith), a Dulliau Ffurfiol (Seiberddiogelwch , Technoleg Blockchain, dilysu Systemau Rheoli Rheilffordd).

Mae'r ymchwil ar Systemau Rheoli Rheilffyrdd wedi arwain at ffurfio Grŵp Gwirio Rheilffyrdd Abertawe a gyflwynodd Astudiaeth Achos Effaith hefyd.

Mae is-grŵp arall yn ddiweddar yn astudio Sefydliad Addysgol, Hanesyddol ac Athronyddol Cyfrifiadureg.

Cyfryngau cymdeithasol

Blog- http://www.cs.swansea.ac.uk/theory/

Seminar Calendar- https://www.cs.swansea.ac.uk/theory/index.php/calendar/

Staff Cysylltiedig

Prof Arnold Beckmann,

Dr Ulrich Berger,

Dr Jens Blanck,

Dr Liang-Ting Chen,

Dr Xiuyi Fan,

Dr Phillip James,

Dr Oliver Kullmann,

Prof Faron Moller,

Dr Berndt Muller,

Dr Arno Pauly,

Dr Liam O'Reilly,

Dr Jean-Jose Razafindrakoto,

Gweld proffiliau yma- http://www.cs.swansea.ac.uk/theory/index.php/people/

Prof Markus Roggenbach,

Dr Monika Seisenberger,

Dr Anton Setzer,

Prof John V Tucker,

Dr Ferdinand Vesely,

Dr Adam Wyner

Cyhoeddiadau

A selection of publications:

Beckmann, A. & Preining, N. (2018). Hyper Natural Deduction for GÃ¶del Logicâ€”A natural deduction system for parallel reasoning. Journal of Logic and Computation 28(6), 1125-1187.
Beckmann, A., Buss, S., Friedman, S., Moller, M. & Thapen, N. (2018). Feasible set functions have small circuits. Computability, 1-32.
Beckmann, A. & Razafindrakoto, J. (2017) Total Search Problems in Bounded Arithmetic and Improved Witnessing. In Logic, Language, Information, and Computation. (pp. 31-47). Springer.
Beckmann, A. & Buss, S. (2017). The NP Search Problems of Frege and Extended Frege Proofs. ACM Transactions on Computational Logic 18(2), 1-19.
Beckmann, A. & Preining, N. (2017). Deciding logics of linear Kripke frames with scattered end pieces. Soft Computing 21(1), 191-197.
Berger, U. & Petrovska, O. (2018) Optimized Program Extraction for Induction and Coinduction. In Sailing Routes in the World of Computation. -80). Kiel, Germany: Springer.
Berger, U., James, P., Lawrence, A., Roggenbach, M. & Seisenberger, M. (2017). Verification of the European Rail Traffic Management System in Real-Time Maude. Science of Computer Programming
Berger, U. & Hou, T. (2016). A realizability interpretation of Church's simple theory of types. Mathematical Structures in Computer Science, 1-22.
Berger, U. & Spreen, D. (2016). A coinductive approach to computing with compact sets. Journal of Logic and Analysis
Berger, U. Blanck, J. & Kober, P. (2010). Domain representations of spaces of compact subsets. Mathematical Structures in Computer Science 20(02), 107
Bauer, A. & B., Jens (2010). Canonical effective subalgebras of classical algebras as constructive metric completions. Journal of Universal Computer Science 16(18), 2496-2522.
Blanck, J., Stoltenberg-Hansen, V. & Tucker, J. (2008). Stability for Effective Algebras. Electronic Notes in Theoretical Computer Science 221, 3
Blanck, J. (2008). Reducibility of domain representations and Cantorâ€“Weihrauch domain representations. Mathematical Structures in Computer Science 18(06), 1031-1056.
Blanck, J. (2005). Efficient exact computation of iterated maps. The Journal of Logic and Algebraic Programming 64(1), 41
Urbat, H., Adamaek, J., Chen, L.-T., Miliua, S. (2017). Eilenberg Theorems for Free. Proceedings of MFCS.
Zhong, Q., Fan, X., Luo, X. & Toni, F. (2019). An explainable multi-attribute decision model based on argumentation. Expert Systems with Applications 117, 42-61.
Fan, X. (2018) On Generating Explainable Plans with Assumption-Based Argumentation. In PRIMA 2018: Principles and Practice of Multi-Agent Systems. (pp. 344-361).
Fan, X. (2018). PRIMA 2018: Principles and Practice of Multi-Agent Systems. Tokyo: The 21st International Conference on Principles and Practice of Multi-Agent Systems.
Fan, X., Zhang, H., Leung, C. & Shen, Z. (2018) Fall Detection with Unobtrusive Infrared Array Sensors. In Multisensor Fusion and Integration in the Wake of Big Data, Deep Learning and Cyber Physical System. (pp. 253-267). Springer.
Zeng, Z., Fan, X., Miao, C., Leung, C., Jih, C. J. & Soon, O. Y. (2018). Context-based and Explainable Decision Making with Argumentation. Presented at Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems.
James, P. & Roggenbach, M. (2014). Encapsulating Formal Methods within Domain Specific Languages: A Solution for Verifying Railway Scheme Plans. Mathematics in Computer Science 8(1), 11-38.
James, P., Moller, F., Nga N., Roggenbach, M., Schneider, S. & Treharne, H. (2014). On modelling and verifying railway interlockings: Tracking train lengths. Science of Computer Programming 96, 315-336.
James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S. & Treharne, H. (2014). Techniques for modelling and verifying railway interlockings. International Journal on Software Tools for Technology Transfer 16(6), 685-711.
James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M. & Williams, D. (n.d.) Verification of Scheme Plans Using CSP $$||$$ | | B. In Software Engineering and Formal Methods. -204).
Abbasizanjani, H. & Kullmann, O. (0). Minimal unsatisfiability and minimal strongly connected digraphs. Presented at Theory and Applications of Satisfiability Testing - SAT 2018, Oxford, UK: Theory and Applications of Satisfiability Testing.
Heule, M.., Kullmann, O. & Biere, A. (2018) Cube-and-Conquer for Satisfiability. In Handbook of Parallel Constraint Reasoning. (pp. 31-59). Springer.
Heule, M. & Kullmann, O. (2017). Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method. Presented at 26th International Joint Conference on Artificial Intelligence (IJCAI 2017),, 4864-4868. Melbourne, Australia: International Joint Conference on Artificial Intelligence (IJCAI).
Heule, M.. & Kullmann, O. (2017). The science of brute force. Communications of the ACM 60(8), 70-79.
Heule, M., Kullmann, O. & Marek, V. (2016) Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre (Ed.), Theory and Applications of Satisfiability Testing â€“ SAT 2016. (pp. 228-245).
Moller, F. & Powell, S. (2018). Teaching Computing via a School Placement. Presented at Computing Education Practice, Durham, UK: Computing Education Practice.
Moller, F. & Crick, T. (2018). A university-based model for supporting computer science curriculum reform. Journal of Computers in Education 5(4), 415-434.
Crick, T. & Moller, F. (2015). Technocamps: : Advancing Computer Science Education in Wales. Presented at 10th Workshop in Primary and Secondary Computing Education,, 121-126.
Moller, F. & Crick, T. (2016).A National Engagement Model for Developing Computer Science Education in Wales. Presented at ISSEP'2016: The 9th International Conference on Informatics in Schools, Munster, Germany: ISSEP 2016.
Chilton, C., Kwiatkowska, M., Moller, F. & Wang, X. (2016) A Specification Theory of Real-Time Processes. In Concurrency, Security, and Puzzles. (pp. 18-38).
Williams, S., Ware, J M. & Müller, B. (2018). Preserving safety, privacy and mobility of persons living with Dementia by recognising uncharacteristic out-door movement using Recurrent Neural Networks with low computing capacity. Proceedings of the First Joint Workshop on AI in Health.
Moller, B. (2017). Chapter: Technology futures. (2017). In: Securing the future: planning health and care for every generation. Pages 26-31. Future Care Capital.
Williams, S. & Moller, B. (2017). Agents and Dementia “ Smart Risk Assessment. In: Multi-Agent Systems and Agreement Technologies. LNAI 10207, pages 277-284.
Abdullahi, I. & Moller, B. (2017). Towards Efficient Verification of Elementary Object Systems. Proc. Concurrency, Specification, and Programming (CS&P 2016). CEUR Workshop Proceedings, Vol-1698 (urn:nbn:de:0074-1698-4), pages 86-100.
Betts, J. & Moller, B. (2017). A Component-based C++ Framework for Developing BDI Agents. Proc. SAI Intelligent Systems Conference. 877-883. IEEE, 2015.
Pauly, A. (2018). Parameterized Games and Parameterized Automata. Electronic Proceedings in Theoretical Computer Science 277, 30-42.
Basset, N., Jecker, I., Pauly, A., Raskin, J. & van den Bogaard, M. (2018). Beyond Admissibility: Dominance Between Chains of Strategies. Computer Science Logic (CSL). doi:10.4230/LIPIcs.CSL.2018.10
Pauly, A. (2018). Enumeration Degrees and Topology. Presented at Sailing Routes in the World of Computation,, 228-337. doi:10.1007/978-3-319-94418-0_33
Le Roux, S., Pauly, A. & Raskin, J. (2018). Minkowski Games. ACM Transactions on Computational Logic 19(3), 1-29.
Pauly, A., Fouche, W. & Davie, G. (2018). Weihrauch-completeness for layerwise computability. Logical Methods in Computer Science 14(2)
Blasco, J., Chen, T., Muttik, I. & Roggenbach, M. (2017). Detection of app collusion potential using logic programming. Journal of Network and Computer Applications
Blasco, J., Chen, T., Kalutarage, H., Muttik, I., Nguyen, H., Roggenbach, M. & Shaikh, S. (2017). Detecting Malicious Collusion Between Mobile Software Applications: The Android TM Case. In Data Analytics and Decision Support for Cybersecurity.
Knapp, A., Roggenbach, M. & Schlingloff, B. (2015). Automating Test Case Selection in Model-Based Software Product Line Development. International Journal of Software and Informatics 9(2), 153-175.
Knapp, A., Mossakowski, T., Roggenbach, M. & Glauer, M. (2015) An Institution for Simple UML State Machines. In Fundamental Approaches to Software Engineering. -18). Springer.
Schwichtenberg, H., Seisenberger, M. & Wiesnet, F. (2016) Higmanâ€™s Lemma and Its Computational Content. In Advances in Proof Theory. (pp. 353-375).
James, P., Lawrence, A., Roggenbach, M. & Seisenberger, M. (2016) Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude. In Formal Techniques for Safety-Critical Systems. Springer.
Berger, U., Jones, A. & Seisenberger, M. (2015). Program extraction applied to monadic parsing. Journal of Logic and Computation, exv078
Abel, A., Adelsberger, S. & Setzer, A. (2017). Interactive programming in Agda â€“ Objects and graphical user interfaces. Journal of Functional Programming 27
Kanso, K. & Setzer, A. (2016). A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science 26(01), 129-153.
Kanso, K. Moller, F. & Setzer, A. (2009). Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science 250(2), 19
Abdul Rauf, R., Berger, U. & Setzer, A. (2008). A Provably Correct Translation of the Lambda-Calculus into a Mathematical Model of C++. Theory of Computing Systems 43(3-4), 298-321.
Dybjer, P. & Setzer, A. (2006). Indexed inductionâ€“recursion. The Journal of Logic and Algebraic Programming 66(1), 1
Tucker, J., Beggs, E., Cortez, P. & Costa, F. (2018). Classifying the computational power of stochastic physical oracles. International Journal of Unconventional Computing
Tucker, J. (2017). Richard Price and the History of Science. Transactions of the Honourable Society of Cymmrodorion 23, 69-86.
Wang, V. & Tucker, J. (2017). Surveillance and identity: conceptual framework and formal models. Journal of Cybersecurity 3(3), 145-158.
Tucker, J., Johnson, K. & Wang, V. (2017). Theorising Monitoring: Algebraic Models of Web Monitoring in Organisations. Presented at Lecture Notes in Computer Science,, 13-35. Berlin: Springer Verlag. doi:https://doi.org/10.1007/978-3-319-72044-9_3
Wang, V. & Tucker, J.. (2016). Phatic systems in digital society. Technology in Society 46, 140-148.
Vesely, F. (2016). Towards Small-step Compilation Schemas for SOS (extended abstract). In L. Aceto, I. Fabregas, A. Garcia-Perez, and A. Ingolfsdottir, editors, Proceedings of the 27th Nordic Workshop on Programming Theory, NWPT 2015.
Mosses, p. & Vesely, f. (2015). Weak Bisimulation as a Congruence in MSOS. In N. MartÃ-Oliet, P. C. Ã–lveczky, and C. Talcott, editors, Logic, Rewriting, and Concurrency, volume 9200 of Lecture Notes in Computer Science, pages 519â€“538.
Mosses, P. & Vesely, F. (2014). FunKons: Component-Based Semantics in K. In S. Escobar, editor, Rewriting Logic and Its Applications, volume 8663 of Lecture Notes in Computer Science, pages 213â€“229. Springer International Publishing, 2014.
Wyner, A. (2016). A functional perspective on argumentation schemes. Argument & Computation 7(2-3), 113-133.
Shulayeva, O., Siddharthan, A. & Wyner, A. (2017). Recognizing cited facts and principles in legal judgements. Artificial Intelligence and Law 25(1), 107-126.
Wyner, A., Bench-Capon, T., Dunne, P. & Cerutti, F. (2015). Senses of â€˜argumentâ€™ in instantiated argumentation frameworks. Argument & Computation 6(1), 50-72