Browsing by Author "Muller, Moritz Martin"
Now showing items 17 of 7

A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Chen, Yijia; Muller, Moritz Martin; Yokoyama, Keita (Association for Computing Machinery (ACM), 2018)
Conference report
Open AccessThe complexity of the parameterized halting problem for nondeterministic Turing machines pHalt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, ... 
A remark on pseudo proof systems and hard instances of the satisfiability problem
Maly, Jan; Muller, Moritz Martin (20181120)
Article
Open AccessWe link two concepts from the literature, namely hard sequences for the satisfiability problem sat and socalled pseudo proof systems proposed for study by Krajícek. Pseudo proof systems are elements of a particular ... 
Automating resolution is NPHard
Atserias, Albert; Muller, Moritz Martin (202009)
Article
Open AccessWe show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NPhard. In the parlance of proof complexity, Resolution is not automatable unless P = NP. Indeed, we ... 
Automating Resolution is NPhard
Atserias, Albert; Muller, Moritz Martin (Institute of Electrical and Electronics Engineers (IEEE), 2019)
Conference report
Open AccessWe show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NPhard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, ... 
Feasibly constructive proofs of succinct weak circuit lower bounds
Muller, Moritz Martin; Pich, Ján (202002)
Article
Open AccessWe ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial ... 
Polynomial time ultrapowers and the consistency of circuit lower bounds
Bydžovský, Jan; Muller, Moritz Martin (2020)
Article
Open AccessA polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory ∀PV of all polynomial time functions. Generalizing a theorem of ... 
The parameterized space complexity of modelchecking bounded variable firstorder logic
Chen, Yijia; Elberfeld, Michael; Muller, Moritz Martin (2019)
Article
Open AccessThe parameterized modelchecking problem for a class of firstorder sentences (queries) asks to decide whether a given sentence from the class holds true in a given relational structure (database); the parameter is the ...