aboutlogic #07 | Alexander Steen – Interactive Theorem Provers, Legal Reasoning, Non-Standard Logics

00:00:00: As you already saw about logic, really ask the questions where people can fight.

00:00:05: What's your favorite to improve?

00:00:07: So let me come up with something less problematic namely law when things are easy and there no disagreements so

00:00:22: great

00:00:22: that you tuned into our next episode of About Logic!

00:00:26: And we have a great guest today here named Alexander Steen from The University of Greifswald Where he is professor for computer science.

00:00:34: And he's a professor for the best kind of computer science, namely theoretical computer science.

00:00:40: Like with symbolic artificial intelligence?

00:00:44: Yeah thank you very much that you joined us!

00:00:45: It is a pleasure to be here.

00:00:46: thanks for the invitation.

00:00:49: So would you like to give us like a very brief two-minute quick introduction what does your research about whether are working on?

00:00:57: If we don't keep time?

00:00:59: I promise not.

00:01:05: So I'm in the broad area of automated reasoning, more focused on automated reasonings.

00:01:16: This is a field where we try to develop methods and also implement them under computer that automate logical reasoning.

00:01:25: so the main question has given us some set like in math, right?

00:01:33: I want to have a computer system that does the proof for me.

00:01:37: That some formula actually follows from these assumptions.

00:01:42: I guess everybody who has studied math or studied research knows most proves are probably done by hand.

00:01:49: so if you think about it how do prove it?

00:01:52: get a proof idea write all down.

00:01:53: hope its correct and the hope at least is We'll find the proof automatically without any guidance from the user.

00:02:09: My main focus is development of these kinds of systems, we know that in general they cannot exist because some limits are established for automation and some undecidability results but nevertheless were quite well in practice.

00:02:28: And so this is the main topic and second half of the picture.

00:02:35: Well, that's just the application of these kinds of formalisms in application domain.

00:02:43: So I've been very interested now since there was a Luxembourg in automated normative reasoning which means automatic reasoning but not necessarily with respect to mathematical notions norms and I want to show that maybe some obligations on this side follow or some permissions, so whatever.

00:03:03: Some kind of normative statements And uh... This is a very interesting topic because it's much more complex.

00:03:09: i think at least Yeah!

00:03:12: So this roughly my area.

00:03:15: That the question.

00:03:16: for first part..I mean im working with interactive proof systems.

00:03:22: So there the user drives the proof, but it's convenient if sort of trivial goals are automatically disproved.

00:03:35: What do you think about this?

00:03:37: Yes

00:03:38: I think that truth is as always somewhere in the middle.

00:03:42: so i think we want to have both because we know from experience Most of the time, the thing that you actually want to prove is very complex.

00:03:53: Otherwise he wouldn't bother using this system anyway.

00:03:57: and if it's complex there a good chance that automated systems will never find proof because we know its undecidable even though they are true.

00:04:12: And the advantage, of course with interactive proof systems is that you as a human user have a proof idea and you just have to convince The machine.

00:04:20: That your proof was actually correct.

00:04:22: Just this you say.

00:04:23: I mean there are often steps in large approves might seem trivial for us or they're actually easier than we thought.

00:04:33: So it's nice to just during writing down the proof in a proof assistant prove that by itself.

00:04:43: If not, well then I have to refine and do some you know top-level proof structure And Then i can try again.

00:04:50: but actually this kind of interaction between two kinds Of systems there's the most fruitful approach Because we don't want to prove A plus B equals b plus a all the time.

00:05:01: This is something That won't automate away right?

00:05:08: Or using it in an algebraic derivation which can be quite annoying.

00:05:15: Actually, it's not just about proving things It is about constructing things.

00:05:19: So I find that interactive proof systems help me with discovering the theorem.

00:05:27: I mean formulating its definitions and interactively working with them.

00:05:33: so it isn't just proving something.

00:05:36: a system an automatic system Not a deductive system could not do because it's really inductive in the general sense, right?

00:05:46: I mean instead of discover some notions.

00:05:50: Yeah that is true.

00:05:52: usually this kind of interactive tools you have whole spectrum to apply.

00:06:00: so there are some tools for simplifying goals sometimes for proving small goal.

00:06:05: they will be automated the improvers Probably also.

00:06:08: some tools for checking for counter examples of finding counter models.

00:06:13: And I fully agree with you when thinking about a theory, when constructing something.

00:06:19: so in the process of actually think about things that we want to talk about often using tools that give you counter example are probably most helpful ones to clarify your own way understanding of the matter that you're actually working with.

00:06:38: So, it can extract some kind of corner cases or hidden assumptions that haven't written down because they have not thought about them yet and I think both right?

00:06:48: You need tools to reflect on your current assumption.

00:06:54: other tools help in a broader sense for proving stuff but yeah also Automated tools that do not prove but actually find counter examples.

00:07:04: I mean they are both equally important, yeah.

00:07:07: So

00:07:08: maybe Dennis

00:07:10: want to say something.

00:07:13: maybe continue with the online because i would go for The other half of your.

00:07:17: no i was going for okay Okay Maybe there's a question what is your faith?

00:07:21: I mean Are you using?

00:07:22: i mean i think you're involved in the paper which Is using isabel.

00:07:26: uh This is your favorite proof system.

00:07:29: or have you looked at it?

00:07:33: Do you know something like lean or walk as it's called now?

00:07:38: Yeah, right.

00:07:39: So this is a mean question because regardless of what I say I will infuriate somebody.

00:07:47: let just say Isabel is the system that I've worked most with and also that i have been introduced first when I was student.

00:07:57: It's a proof language of Isabel.

00:08:02: That gives you both the tactic stuff, that applies some kind of rules but also this structured proof format ESA it is called and This makes us quite suitable for teaching about proofs or structural proof because we have more-or less one to one correspondence between by contradiction always could look like this is in structured EZR template or proof-by-cases, and I'm not saying that other assistants don't have it.

00:08:40: This system has worked a lot with Lean at Hall Light, Hall Four and Cork on Rock.

00:08:55: With systems like Rock, it's probably harder to master them but get to a level where you can actually productively apply them because the underlying theories are also bit more complicated.

00:09:09: Because sometimes if we want just talk about some kind of functions and prove something that don't wanna think about dependent types or all the underlying... underlying complexities, I'm not saying that you probably have to understand all this but it feels a bit overwhelming maybe at first.

00:09:27: But also work with Crockback then and actually like the interface quite lot.

00:09:36: so...I think i don't have a preferred system?

00:09:39: Probably they are useful for different or maybe slightly different applications.

00:09:50: I mean, it's a while ago that they used Isabel.

00:09:53: But if you want to focus on representing structures in mathematics...I mean, Isabel is good for deductive reasoning as we say.

00:10:05: but If you're interested in formalizing structural mathematics like reasoning and whatever categories I have some issues with Isabel, but let's not get too deep into this in the moment.

00:10:25: Of course one of the most important points is that my Prover, the Leo III Prover is integrated... ...in the Sledgehammer II of Isabel.

00:10:33: so because if you want to use Leo then you can use Isabelle and Eroket right?

00:10:39: So what exactly is Leo then?

00:10:41: Leo isn't automated the improver.

00:10:43: This is integrated like in the portfolio of solving proof goals in Isabel.

00:10:52: It's an automated theme prover for high order logic, which is also the language of Isabel and I think it was integrated somewhere in twenty or before.

00:11:04: so...I mean its not like a very mature system.

00:11:08: that are the standard tools like CBC and Z three and eProver whatever they're called right?

00:11:18: because it's more or less now a one-man show developing you three, but for some applications that actually gives some good results and I think quite nice proofs.

00:11:28: So yeah... I'm all in favor of course using my tool.

00:11:33: Sure!

00:11:33: That

00:11:34: was the

00:11:36: very minor point.

00:11:38: nowadays is about groups.

00:11:40: after your automated prove us anyways right?

00:11:43: In the first milliseconds we proved so much windows, so just try our tent

00:11:51: to get the best results.

00:11:52: There's no reason for not doing it right because we have the computational power and we have multiple cores.

00:11:58: that would be naive but don't try different approaches all at once.

00:12:04: Great!

00:12:04: So as you already saw about logic really asked questions where people can fight what is your favorite tier improver?

00:12:13: Let me come up with something less problematic namely law.

00:12:20: There are no disagreements.

00:12:24: How can I imagine that?

00:12:26: Did you take the whole legal book and formalize it, then start from there... And how is about different kinds of reasoning when you sit in court?

00:12:37: You normally don't get these lovely clear deductions – you get abduction… It's all messy!

00:12:43: So how can you get this two things

00:12:45: together?!

00:12:48: Probably you can't.

00:12:49: That's the short and simple answer, but no I mean...I still feel like i'm scratching at the surface.

00:12:56: now have been looking into normative reasoning for quite some time.

00:13:02: I started doing this in two thousand eighteen or nineteen years ago.

00:13:09: so we need to be careful when talking about normative reasoning.

00:13:13: of course applications in a legal context because they are Some things that are different, right?

00:13:18: I mean of course probably in all legal processes there is some kind of normative thing involved but the other way around it's not necessarily the case.

00:13:29: So i start looking at non-classical logics which have been designed for dealing with normative information and this what would say?

00:13:40: so the automation of them or creating new logic but really automating.

00:13:46: So this also means that I'm really no expert in how to choose which logic is the most appropriate for representing some kind of stuff.

00:13:59: For real use cases, it's a very hard question.

00:14:05: but then again after just looking at... At the logical course, at actually automation process of normative reasoning I wanted to do something with it that feels a bit helpful.

00:14:18: So i looked at German legal processes and what we could do in such kind of technology in this context?

00:14:29: And i've been contact close collaboration.

00:14:36: I'm not saying that, right?

00:14:37: He's a notary.

00:14:38: This is something completely different.

00:14:40: at least he told me that and for quite some years i've been explaining logic to him And he has been explaining legal topics To Me.

00:14:52: now think it actually took more than couple of months until we actually agreed Some common consensus For the usage Of notions and phrases terminology that we actually are talking about the same thing, which is a very non-trudal I think.

00:15:12: And then of course when you apply stuff to topics from the real world it becomes more complicated.

00:15:19: so was the first point where i learned what's different and now difficulties in really legal process.

00:15:35: But the goal is probably not to automate.

00:15:38: You know, like have a judge automaton or something where we automate in our court case.

00:15:44: but you want some kind of assistance systems that can help be human for decision making.

00:15:51: so we looked at certain steps in legal process when think there's actually logic based AI reasoning tools and this could before discovery of relevant norms that can be for checking whether some kind of argumentation is consistent within itself with respect to a framework.

00:16:17: Because usually the problem, it's not.

00:16:21: you want to verify that some sort of court ruling is correct which cannot do in any way because judges are independent and one judge would probably come for a very different outcome than another judge would.

00:16:38: But both are right, because they're judges and do whatever they do then reach the conclusion or some kind of verdict...

00:16:50: The judge will take an intent on the law into account.

00:16:55: what is intended not so much about deductive conclusions

00:17:02: Exactly.

00:17:02: So we have the problem, so what does norms actually mean?

00:17:06: Do you have open textures?

00:17:07: or when it says vehicle is really meant... When we think about vehicles as a legal term and what's subsumed by that?

00:17:18: but not, at some point you can choose whether to apply this norm whether you think that there's some kind of case where it makes more sense to apply another norm, because you judge the situation to be different.

00:17:34: So

00:17:35: do we judge at the intent as a lawmaker was exactly this?

00:17:42: Exactly!

00:17:44: And so I think the thing that we can probably check The argumentation of a judge is somehow non-conflicting with some kind of legal constraints.

00:18:00: But, we could not really construct the legal outcome because it's so intricately dependent on which path you take through this whole network.

00:18:11: but maybe we can show that a pathway taken there was actually allowed.

00:18:15: and I mean... We have this phrase called Rechtsbeugung.

00:18:23: You're not applying law as you should do.

00:18:26: I

00:18:26: have no idea what's it called?

00:18:31: Bending the law, maybe... I don't know.

00:18:34: and of course this is not allowed because judges are independent but they had to adhere to a law.

00:18:42: Maybe some kind of verification or sanity check if, you know the argument is within the scope of the law or with an intent off-the-law.

00:18:56: And this is probably interesting things that I am step by step looking at.

00:19:00: The

00:19:00: next question we have got some bad history right?

00:19:06: Yes!

00:19:08: Exactly.

00:19:10: but also other applications could be intelligent way looking for the most probable applicable norms because there are a lot of... I mean, there's lots of norms out there.

00:19:28: Which ones do it take?

00:19:29: Maybe its already a simplification or process.

00:19:34: if you can use this tool to find you in a semantical sense the right norms that might be applicable in your case.

00:19:43: so probably as an illegal expert you'll have them on your mind.

00:19:48: Anyway, but maybe you forgot some special rules or so.

00:19:53: I mean some kind of a system systems right?

00:19:56: Sorry the term is perversion of justice.

00:19:59: Perversion

00:19:59: of Justice!

00:20:00: Ah okay well that sounds suitable

00:20:06: yeah.

00:20:06: Yeah obviously in this area if your competition with machine learning and large language models Which, I mean...I'm not working in this area.

00:20:19: But to me there seemed be a better match To legal reasoning than sort of formal system.

00:20:45: from these epistemic logics you take into account.

00:20:52: Maybe by the time it's non-ideal or a non mathematical logic, right?

00:20:56: I think depends on who your ask!

00:20:58: Also i heard expressive logics and domain specific logics... I think that is always perspective of

00:21:06: what we are talking about.

00:21:07: To me point here is epistemy which is actually human reasoning whereas in mathematics, whether it's platonic or not we want to have a good idea about that sounds very platonic.

00:21:24: So as possible approximation on what do you mean by mathematical reasoning?

00:21:32: But this is different from normative deontic and so-on reasoning quite a different area.

00:21:44: And so my thesis is that in mathematics and for mathematical logic, let's say it the logic in mathematics.

00:21:52: Well, mathematics isn't just mathematics a step to computer sciences or physics whatever.

00:21:57: yeah there I want too use a formal system.

00:22:03: but i have my doubts whether the formalization of epistemic logics I mean like the logic of discovery was also attempted, right?

00:22:14: And logic inductive logics and so on.

00:22:17: That this is something...I'm not convinced that it's sort-of very helpful to formalize this.

00:22:26: Well i guess always depends what kind of goal you have in mind.

00:22:32: Usually these kinds of... I call them non classical logics but I see they can be disputed arise and die somehow, like every year there are a lot of logics that have been created.

00:22:47: And probably not being looked at again in the context of AI applications because in AI applications you usually have some kind very specific application scenario in mind if want to model it... ...and then you need an agent or logic that can deal with agents maybe their knowledge maybe communication Create a new logic that has all these kinds of variants because you want to model that kind of scenario.

00:23:15: And, um... Of course this kind of logics they come and go.

00:23:21: I don't know how many logics are being created in you every year at conferences like Ichkai or Ikai whatever.

00:23:30: But those types of logsics have use case-in-mind a nice idea to have some kind of abstract description on what you want to achieve, but that doesn't necessarily mean this logic is already the Holy Grail.

00:23:47: That it can do these kinds of stuff... But again there's an approximation for real-world challenges we actually wanted to look at because real world sounds a bit floppy.

00:24:05: problems are often much more complex than mathematical issues when you also need to incorporate some kind of human factors, physical factors or whatever and they can try to model that well.

00:24:22: So there tools I think automating them.

00:24:29: these kinds of logics build an AI system where it's not all about machine learning and data-driven statistical inference, but you want maybe to have some kind of assurance.

00:24:44: Some checking actions or hybrid approach that can play the strengths and weaknesses in both worlds somehow intermingled with one system?

00:24:56: But what we're saying here seems like a classic AI approach.

00:25:03: So there is this new, I mean sort of machine learning idea which...I was interested in AI as a student but then I drifted off into logic and theoretical computer science.

00:25:19: And so isn't the challenge that these statistical methods are actually working much better in these fuzzy areas?

00:25:32: and do we need this old AI which you defend?

00:25:40: Again, it really depends on what you want to do.

00:25:46: I see the point that for a lot of applications with ML systems they seem to deal quite well with some kind of problems that we couldn't dream off, you know attacking.

00:26:01: But then again for Some kind of simple applications They really don't work.

00:26:06: Well maybe you want to have a system is some kind Of so what I call it mission critical?

00:26:13: i mean this can mean anything like healthcare legal whatever context where really to be sure what your AI system is doing.

00:26:25: Sorry,

00:26:27: because you have to believe in this so formal logic which has maybe not much help.

00:26:35: I mean especially if we now look at the legal business and a practitioner like your colleague here.

00:26:50: Does he really understand this?

00:26:53: I mean, do you really understand how this logic matches with the sort of more intuitive informally.

00:27:02: Right

00:27:03: right!

00:27:05: So what i think is probably that you want to have both because in some kind or in our core You want to make sure that some kind of very low-level steps, of low level reasoning steps are sound.

00:27:22: That the system is really just doing what it's supposed do if there's complex... But what you're

00:27:26: supposed to do?

00:27:27: It's a hard thing!

00:27:29: Do we not create an illusion of realliability?

00:27:38: because in the end logic itself may be not completely transparent Sure.

00:27:45: But then we're not doing any worse than the ML systems, right?

00:27:48: I mean...

00:27:49: No you are in a way because the ML system is more emulating this sort of fuzzy reasoning humans do and if you think about especially supporting legal experts obviously looking at large data by a base-of-cases That seems to be very much in the domain of an LLM or a machine learning system.

00:28:20: But yeah, I mean for things that you can learn?

00:28:23: Yeah sure!

00:28:24: What's the point of learning some kind of norms where we already know what the norms are when maybe we can perfectly describe them and then have it written down as symbolic form okay not logical

00:28:41: one.

00:28:42: Sorry, it's about clearly the application.

00:28:44: I mean a match is just this case right?

00:28:46: This something which legal student has to learn and they learned actually in very...I don't know i'm not really your students..i know somebody who is but maybe we should discuss with them.

00:29:05: But it's much based on looking at cases, learning from examples.

00:29:18: I'm

00:29:21: talking about the devil here because... Yeah,

00:29:28: but then again I mean there is at least in the German legal concept or so if you study this in Germany.

00:29:40: There's what they call rechtslogik So legal logic Part of i think What They Call Rechtsdogmatik.

00:29:49: You Know All The Things How They're Supposed to Work?

00:29:51: I Mean Everybody Knows That In Practice They Probably Don't Work Like that.

00:29:54: But This Is The Ideal And the hope, of course.

00:29:58: At least that's what I think is at the heart of this legal logic... ...at least it describes in these big books some sort of progress going on where you use some kind of inference from this and that.

00:30:20: Of course not as formal like a logician would like that but still Some kind of ideal, where we all know that this is not work in practice.

00:30:30: But there's at least the kind... I mean they claim to be very objective with respect how their deduction process or inference project works In practice.

00:30:52: i would doubt it actually really objective So objective that it can be done in logic.

00:30:59: But I think some aspects of this kind behavior, these kinds steps are going on there can actually describe the logic and i find interesting to have a model that matches maybe not all but most or at least some relevant notions.

00:31:21: I think when we have automation for this kind of stuff, um We could at least try to somehow combine the strength off these kinds of symbolic approach and a kind of Machining approach should do some fuzzy reasoning with ml And maybe to have some kind of reasoning involved and see Atleast if they're conflicting or not To at Least Have Some Kind Of Education Whether You Should Probably Look Closer Or If There Is I don't know if there's no conflict going on, and we will maybe be able to trust the output of this system or so.

00:31:58: I mean i'm not saying that this is you know how degraded right?

00:32:01: I wonder whether it was also related... I think German laws mainly in the Roman law are deductive whereas I live in UK where Gamanic more case-based And I wonder if this is an impact on the right logic of law here.

00:32:20: Yes,

00:32:20: definitely!

00:32:21: So i've seen a lot papers about.

00:32:25: you know AI in Law as it's relatively big community and have very active conferences there... ...and also been part these conferences for sometimes.... ...and they had some papers case law or non-case law systems, but I have to be honest.

00:32:44: I mean i'm not in the details and couldn't really understand that back then.

00:32:49: so definitely there's you know a clean cut.

00:32:52: at least it feels like a clean card for methods which are more applicable on one side than another.

00:32:56: To

00:32:59: put your skepticism into question is oversimplified.

00:33:04: if somebody tells This legal aspect is part of your life.

00:33:08: Let's say a judgment whether you were guilty or not and this part was checked either by real judge, by LLM or by a theory improver.

00:33:20: What would you

00:33:22: choose?

00:33:23: I mean it's not how it works but

00:33:24: for the judged.

00:33:31: But

00:33:32: the judge is overworked and we have an issue with especially asylum cases which creates lots of excitement.

00:33:44: There's a big backlog because there are not enough judges.

00:33:48: so yes, you need to make it more efficient right?

00:33:54: The question isn't too much some computer, but how can we support as a judge and the legal professionals most effectively?

00:34:07: I have to admit that my feeling or my preliminary conclusion is that LLMs would be much better suited for this than an epistemic logic.

00:34:29: I would be worried about hallucinations.

00:34:31: Sure, but I'm very... Things

00:34:33: like that which i would be less worried in case of theory progress.

00:34:37: No no!

00:34:38: I am worried about the theorem prover because it gives you an illusion of reliability.

00:34:44: where there is a mismatch Is then whether the logic actually corresponds to what we want And thats much more dangerous.

00:34:58: But if the deductive system promises, oh this is a conclusion.

00:35:03: You are now going to be executed because according to these logic you should die.

00:35:12: so come on!

00:35:15: Yeah I mean there are deontic logics where i can prove that you were allowed to kill somebody just because of some triviality...I completely agree right?

00:35:27: Because this is something that probably also students or experts in fields like computer science and mathematics don't often really have a feeling for, there are many different logics.

00:35:43: They have their subjectivity but hidden into logic the mechanism looks very mathematical objective definitions, how we infer stuff right?

00:35:56: But of course it's built in the axiomatization or rules whatever.

00:36:00: Of the logic.

00:36:02: but yeah I mean...of course.

00:36:05: then again i would say well..I know that why shouldn't the company all the public government who orders this kind of system trust in a logic?

00:36:15: because logic was probably designed for especially a requirement elicitation process, and we should know what it can do or cannot.

00:36:28: I mean this applies for machine learning and logic-based stuff.

00:36:31: equally I would say but yeah...I get the feeling that probably for layman i think its now clear not how everybody has played with Gimini and ChatGPT whatever they are called.

00:36:47: They know there could be spooky things happening here Once you hear, or this is a system that's proved correct.

00:36:57: Whatever it means then probably the level of trust at least subjective level of trusts are much higher and of course... This is danger but for me doesn't necessarily imply these kind tools or methods shouldn't be a suitable addition to the suit of tools we have.

00:37:24: But, it's true in deontic logic research or normative logic research as far I know they still haven't settled on what kind of logic is right?

00:37:37: Logic for doing deontics detachment.

00:37:40: so how should we do legal stuff if you don't really understood deontik in France yet.

00:37:47: So this an ongoing research.

00:37:51: The question posed by Lakatosz, now for the mathematical case what would happen if number theorists prove that Goldbach conjecture holds and we have a deduction that Piano or Arithmetic proved that Goldbach conjectures doesn't hold.

00:38:06: And back then Lakatosch was optimistic that the number theorist will say let's just get rid of Piano-Arithmetic Maybe let's hope that Leibniz covers.

00:38:15: So you mean

00:38:15: the piano is inconsistent or what?

00:38:18: I mean, this was a word speed suggested actually at some point.

00:38:23: Yeah... You don't need full inconsistency right?

00:38:26: We just need one disagreement where Piano-Radmitic

00:38:31: is different

00:38:32: in scope than with number theoretic practice.

00:38:35: so

00:38:36: number

00:38:36: theorists see something they see a proof of written in ordinary language And then they agree, oh this is a lovely proof of Godbust conjecture.

00:38:50: But shouldn't there be able to say what's used in the proof?

00:38:55: Or do

00:38:56: I just

00:38:57: write on the preamble... Oh i use ZFC and maybe Groten Deku... Yeah yeah yeah

00:39:02: but okay!

00:39:03: In that case you should not leave the mathematicians alone with us.

00:39:09: You should call your emergency solution.

00:39:12: So like the

00:39:15: emergency logician number has to be called, you know.

00:39:18: And the emergency logic has two taxes here.

00:39:22: so I mean

00:39:23: they would look from both sides apparently right?

00:39:25: They will see as this formalization really adequate?

00:39:27: or is natural language proof really adequate and similar?

00:39:31: i guess in legal context it's just what alerts if there was disagreement.

00:39:38: But I

00:39:39: made it binary, take this or that.

00:39:41: No

00:39:42: comparison isn't really working.

00:39:46: in mathematics we can boil down things to some sort of ideal reasoning.

00:39:52: In law we count as a different area.

00:39:55: so the analogy is not working.

00:40:00: but still i mean its true.

00:40:07: Just like we said that once you settled on some kind of logic, I mean... Of course.

00:40:12: You have some kind inferences within the type of logic.

00:40:15: but it's really hard to know whether a logical choice is actually right one and this an aspect many people don't think about much.

00:40:27: even in mathematics The idea of the right logic is very problematic.

00:40:34: I mean, that doesn't come in with legal.

00:40:38: but i think the fact that mathematics is striving for sort of some idealized reasoning to what the results can be achieved isn't clear.

00:40:49: and even by striving for this idealized reason it's not clear exactly what principles or axioms we are accepting.

00:40:57: But I think law is really different.

00:41:00: It's really based on human interaction, evolution of culture, evolution ideas and reflecting this so it really is fundamentally different yeah?

00:41:12: So

00:41:13: while... That was probably you want to look at one legal system And within that one legal systems there are some kind of method or at least not for the German

00:41:25: system.

00:41:26: In principle, we have some kind of objective matter in principle how to do some subsumption and come to legal conclusions.

00:41:37: But I agree not the legal process is idealized but i think some portions can be idolised

00:41:50: if somebody checks whether... discussion, but about arithmetic.

00:41:58: and so they are arithmetic and solvents.

00:42:01: And you think that legal people can do arithmetics right?

00:42:05: Do we need real

00:42:06: numbers?!

00:42:07: Is this not Zeno?

00:42:08: You know I can submit always a bit later!

00:42:16: I'm astonished at how it even works after the deadline for quite some conferences... But maybe i shouldn't say this aloud.

00:42:23: A lumpy topic, quite complex one.

00:42:28: We are close to the time limit but this aspect of checking the formalization is what I just wanted say.

00:42:39: maybe that's a reason why we need philosophers.

00:42:41: they should check whether these parts worked out so lot working with concepts.

00:42:47: It's an interdisciplinary endeavor, right?

00:42:49: And computer science legal philosophy.

00:42:51: But then we need a lot of us that are also trained in illegal studies and also trained on chemistry and biology because I mean essentially this knowledge engineering part is really hard part Because you can be usually your next person in logic or in chemistry but probably not both.

00:43:11: But in practice, if you want to use some kind of symbolic representation for... I don't know.

00:43:17: Some reactions are so in biology or biochemistry You need your domain knowledge.

00:43:28: This really calls for interdisciplinary approaches, interdisciplinary studies projects because we need experience and domain knowledge from all these areas.

00:43:42: The last sociological question, maybe.

00:43:45: So you were joked around the lawyer not liking arithmetics and I mean there's some truth to that.

00:43:50: a lot of friends Of mine who studied law said i picked law because they really don't like math And I hoped To get rid off all mouth.

00:43:58: and then There was it?

00:43:59: They Were little annoyed how formalized Like Some parts of their practice where like getting particular style to write this or that document and really needing to fit schema, so-to speak.

00:44:13: So there's a formal element they hope to get rid of but then the edit was back there.

00:44:18: long story short I have you rough feeling how open practitioners are to your kinds off approaches?

00:44:25: Is it something they find interesting?

00:44:27: is there something they hate Something They Are Willing To Open Up Or Once A Black Box Without Looking In?

00:44:35: I Have The Feeling That They're Not Too Happy About It.

00:44:43: I get the point that once you have a feeling, this research would go into direction and make your jobs somehow easier.

00:44:58: Make it meaningless because they can be automated.

00:45:09: We are so far away from doing some kind of automation or semi-automated assessments that this is not going to happen.

00:45:21: But the problem, of course, in practice lawyers need systems that work and we as scientists usually write down research software to demonstrate something, but maybe probably doesn't work in practice that well.

00:45:45: And there's of course a big gap and research software development where we need some kind of you know gluing part between these both worlds make it attractive for the application side actually test some kinds of systems because they don't have go not just one extra mile But You Know A lot of extra miles.

00:46:03: But usually in research, I mean you don't have that many resources to actually care a lot about software and such way they can use it.

00:46:18: They would include industrial style deployment of software with what called the assurance documentation.

00:46:26: we do not have money for this right?

00:46:30: factors including this one that makes it hard in practice to test out the systems and of course, real applications.

00:46:40: Of course there's also a data protection stuff but I think for whatever makes working life easier he or she is happy.

00:46:55: I mean, i would be surprised if it wasn't so.

00:46:58: So in another system that was actually praised as one of the most helpful systems... ...I cannot really recall where the context or what the context is but they had a plug-in for Word or some kind of office product Where there could highlight some legal document and three colors of things that the mayor is allowed to do and what he's a privateer.

00:47:34: The other color was something else, I don't know... And they could now not just press Ctrl F for the phrase fees but look at word fee within red coloring prohibitions about fees, and this was I mean from the research perspective.

00:47:57: This is highlighting a search in color, this trivial right?

00:48:02: But it makes their work much easier.

00:48:05: And of course there are lot these things that have from scientific perspective maybe not so interesting but including like digitalization in general would make they're life much more easy which would be necessary to do the next step, you know.

00:48:21: To really research interesting stuff with them.

00:48:26: but yeah okay.

00:48:27: so one last question Thorsten?

00:48:28: No I think i'm fine.

00:48:30: maybe come to an end

00:48:33: lovely.

00:48:33: then let me say thank you once again for coming here.

00:48:37: take the video donating your time in the very end sure and I hope it was a little bit of fun.

00:48:47: Yes, so subscribe.

00:48:49: I guess you say that not on YouTube and we will have Many more interesting logicians and people around logic here.

00:48:59: for once again Thank You Alex pleasure see you soon.