Research

Publications

  • Quratul-ain Mahesar and Volker Sorge
    Algebraic Theory Exploration: A Comparison of Technologies
    Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - SYNASC 2012 (.pdf)
  • Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen and Volker Sorge
    A Term Rewriting System for Kuratowski's Closure-Complement Problem
    Proceedings of the 23rd International Conference on Rewriting Techniques and Applications - RTA 2012 (.pdf)
  • Quratul-ain Mahesar and Volker Sorge
    Generation of Large Size Quasigroup Structures Using Algebraic Constraints
    Proceedings of the 19th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2012.
    (.pdf)
  • O. Al-Hassani, Q. Mahesar, C. Sacerdoti Coen and V. Sorge
    Solving Kuratowski Problems by Term Rewriting
    Proceedings of the 19th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2012.
    (.pdf)
  • Quratul-ain Mahesar and Volker Sorge
    Property Preserving Generation of Large Size Quasigroup-structures
    Proceedings of the 17th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2010.
    (.pdf)
  • Quratul-ain Mahesar and Volker Sorge
    Classification of Quasigroup-structures with respect to their Cryptographic Properties
    Proceedings of the 16th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2009.
    (.pdf)

Systems and Libraries

  • HR is a system for automated theory formation.
  • TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated theorem proving (ATP) systems.
  • Prover9 and Mace4 Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
  • The E Equational Theorem Prover is a a purely equational theorem prover for full first-order logic.
  • Vampire Theorem Prover proves theorems in first-order logic.
  • Paradox is a finite-domain model finder for pure first-order logic with equality.
  • FINDER (Finite Domain Enumerator) takes as input a first order theory, expressed as a set of clauses, and gives as output the models of that theory with domains of given finite cardinality.
  • MINION is a constraint solver that provides fast, scalable constraint solving.
  • MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.

Math Writing Links

Others