- Alp Bassa (Sabanci University, Istanbul)
- Kazim Buyukboduk (Koc University, Istanbul)
- Safak Ozden (Mimar Sinan University, Istanbul)
- Ayberk Zeytin (Galatasaray University, Istanbul)

- Hakan Ayral (Galatasaray University)
- Merve Durmus (Galatasaray University, Yeditepe University)
- Muhammed Uludag (Galatasaray University )
- Ayberk Zeytin (Galatasaray University )

10.30 - 10.50 Merve Durmus

11.15 - 12.15 Muhammed Uludag

13.45 - 14.45 Ayberk Zeytin

15.00 - 16.00 Hakan Ayral

- Hakan Ayral (Galatasaray University) Title : Automated Theorem Proving Systems
- Merve Durmus (Galatasaray University, Yeditepe University) Title: Subgroups of the infinite dihedral group and graphs
- Muhammed Uludag (Galatasaray University ) Title: Binary quadratic forms as dessins
- Ayberk Zeytin (Galatasaray University ) Title: Thompson's Groups and the Modular Group

Abstract: Automated theorem proving is formal proving of mathematical theorems by computer programs with little or no user intervention.

A formal proof is a proof in which every single logical inference has been checked back to the fundamental axioms of mathematics; first serious attempt to formalize mathematics in terms of symbolic logical inferences was by Russel and Whitehead in their Principia Mathematica, written with a purpose to derive some of the mathematical expressions of number theory.

In a consistent axiomatic system, the validity of a theorem can be expressed as the satisfiability of a logic formula which reduces to a set of propositional satisfiability problems. The problem of deciding the satisfiability of a formula (SAT-problem) varies from trivial to impossible; for the case of propositional logic, the problem is decidable but Co-NP-complete.

First-order theorem proving is one of the most mature subfields of automated theorem proving as first order logic is expressive enough to allow the specification of arbitrary problems, and a number of sound and complete calculi have been developed, enabling fully automated systems.

As part of the talk we will present some of the widely known automated theorem proving softwares and browse through formalizations of some trivial facts (2+2=4, primality of 3) and some non-trivial proofs.

Abstract: In this talk we will show how one constructs a unique graph to every subgroup of the infinite dihedral group, which may be thought of as the toy case of the modular group to be described in the next talk.

Abstract: Since it encodes the Euclidean algorithm, the modular group is a very fundamental object in mathematics. It acts by conjugation on an infinite bipartite planar tree, which we call the Farey tree. The orbits are graphs with one cycle which we call çarks. We show that each çark represents naturally the class of an indefinite binary quadratic form, and every such class can be represented this way. Given a çark, if we specify an edge together with an orientation of its cycle, then this determines an indefinite binary quadratic form belonging to the class represented by the çark, and every such form can be represented this way. This work is funded by TUBITAK110T690 and GSU12.504.001 grants.

(Joint work with M. Durmuş and A. Zeytin)

Abstract: In this talk after defining Thompson's groups F and T via universal Teichmuller theory, we will describe a new point of view on the Thompson's groups (F and T) using the modular group. Then we will discuss the category of carks, a category whose objects are indefinite binary quadratic forms and morphisms are flips.

(this is joint work with M.Uludag.)

IMBM: Istanbul Matematiksel Bilimler Merkezi

© GSÜ Math. Tüm hakları saklıdır.