#747: Unpacking Automated Reasoning: From Mathematical Logic to Practical AI Security

0:00This is episode 747 of the AWS podcast, released on November 24th, 2025. Hello, everyone, and welcome back to the AWS Podcast. I'm Liz here with you. Great to have you back, and I'm joined by a very special guest. I'm joined by Byron Cook, who is a Vice President and Distinguished Scientist here at AWS. G'day, Byron. How are you going? Hey, how's it going? Good, thanks. So you are back. We've had you on the podcast a couple of times years ago now, and it was long overdue to have you back because as is the case with many scientific advancements, the uses are not always evident to the general populace, but as technology changes, stuff happens.

0:46So obviously we're going to talk about Gen AI because you can't not. But first, let's talk about your specific domain, which is automated reasoning, because it is a fascinating domain. not many people know about it when i speak to customers about the concept so let's maybe just briefly unpack that and then we'll get into the utility side so tell us about automated reasoning and why you're so interested in yeah so i mean in the past we would have talked about uh the story would have started in the 70s or 80s about um people attempting to prove programs and and you know we talked about practical applications microprocessor i got my start and microprocessor verification, worked on reasoning about genetic regulatory pathways, reasoning about railway switching systems, reasoning about operating systems, and then Amazon reasoning about policies and virtualization and networking and topography and storage and all that kind of stuff.

1:46But actually, the story goes way back. So Turing actually wrote one of the first papers in the space. It's called How to Prove a Large Routine or How to Check a Large Routine. But he shows basically how to take a program, essentially map it into the program semantics, the world of mathematics, like mathematical logic, and then to reason about the mathematical artifact that the program is actually really representing. And we basically use the same tricks today. But then a really interesting thing happened is that with the invention of the digital computer, people right away began to think, well, like, you know, what about like artificial brains?

2:34And so the term artificial intelligence was coined at this workshop at Dartmouth. It was John McCarthy, I think, hosted it. And they invited folks from kind of different disciplines from cognitive sciences, logic, you name it, statistics, information theory claude shannon was there and um and they they termed they coined that term uh artificial intelligence and so i would that so if you had talked to people in the 60s and asked them what is artificial intelligence it's actually highly likely you would have heard about my area automated reasoning so it's it's the it's the logical it's the manipulation of symbols in a logic system to try and deduce, you know, to try and, and so there's, you know, so the sort of running competition battle or collaboration, if you will, has actually been in these different areas where you have the sort of statistical, like views based on cognitive science on your neurons and so on.

3:42And then views like based on Bayes' theorem, for example. and then views based on mathematical logic. And at various points along the way, the different approaches have been ahead or behind. And I guess they excel at different things too. Like they've got different strengths and weaknesses. Yeah, exactly. And so one of the things that happened is there was this notion of AI winters. So basically for funding, there was a big pendulum swinging back and forth. Like there was tons of funding, there was no funding, there was tons of funding, there was no funding. And so what happened in time is that these different researchers got sort of more and more specific about the exact problem they were taking on with their tools and so the areas kind of diverged and so um so you know machine learning so you know later we would call those tools like machine learning automated reasoning and so automated reasoning uh became the kind of domain of like how do we reason about programs as opposed to how do we like think about you know the reproducing you know artificial general yeah yeah sort of an analogy of human thought and it's interesting because if you think about why this is relevant and why you've been working on this within amazon for so long as well is is we do things that like huge scale like like it's it's it's difficult for a lot of folks to understand the scale that we get to operate at and it's a real privilege to go to do that but when you get to that sort of scale it's kind of beyond anyone's purview to figure out well how do you know this will work like how do you know unexpected things won't happen and this is where this discipline i think really comes into it that this is not about guessing or assuming or it's sometimes okay like this is about will this happen or will this not happen type delineation yeah there's like um at the top of my mind there's sort of three trend lines that drove the adoption of automated reasoning at amazon and then you know i'm sure we'll end up talking about it but then how it becomes neuro symbolic ai and how that connects to gen ai to gen to kai but three big drivers pre pre the general public getting super excited about generative ai the big the big drivers were one there's actually a very radical increase in the capabilities of the most one of the most foundational automated reasoning technologies.

6:02It's called propositional satisfiability solving. So there's an international competition of the tools, and the tools are getting better and better and better, like remarkably so, and there's some real breakthroughs going out there. There's a real breakthrough like around 1999, but then there's some huge breakthroughs like 10 years ago. And so those tools are just getting better and better. So if you encode your problems into the formats these tools can handle, they're way better able to solve them now than they were before. So that's one trend. Another trend is that this move to a services model and the view that software is not shrink-wrapped, it's operated.

6:40And so that drives a different economies of scale situation where you basically are constantly, you're encouraged to constantly rewrite the code, right? So we write some software, we deploy it, we take technical debt we know that the software probably isn't going to be able to scale to where we think it might go but we wait that we see how customers are using it and then we're constantly rewriting that and so that that opens up the uh the desire for the teams to then to want to replace code or to they're constantly rebuilding the code in that so that's an entry point for the formal as opposed to other places i've worked where it's like they wrote it perfectly the first time it was their opinion and so you kind of yeah great it's it's real hard to go and like get them to yeah exactly um and then the um what's the the the the third thing is is that with the move to the cloud um a bunch of conservative security obsessed customers were kind of kind of looked at they looked they looked at the economics and they liked it a lot but they were nervous about security and that this work became the reason they would come that they were actually excited to get off their new jersey data centers say right so they so they they want they wanted to move to aws a because of the cost but they're like oh wow if you can so and we had um customers say you know we'll move orders of magnitude workload over more to aws if you can prove the correctness of the cryptography that's super meaningful to us that's a threat model that were really worried about and uh and so but so so basically it drove a bunch of business into aws um yeah and so i'd say those those three things were the perfect storm and i was just kind of really lucky right place right time when i joined uh amazon well it's interesting too that um you know often often highly complex detailed areas of research like this that are shifting all the time often the jump into the practical side is quite difficult.

8:40And what's been interesting to me is to see automated reasoning sort of dip its toe in the water a little bit within AWS, but suddenly it's like it's available in the hands of every AWS user. So if you're talking about provable security, if you're using different capabilities like trying to understand what can access my VPC, et cetera, you've managed to surface this capability in a, in a consumable form, really. Like our customers get to use this every day, sort of unconsciously. Yeah, I mean, my frustration is that we're not really even giving them the half of it, right? Like the problem we have is that automated reasoning is a little bit of a misnomer because there's actually a spectrum.

9:29So some tools are actually push button fully automated. But traditionally, the scope of the problems they could solve were rather limited and so that's that's what you have with im access analyzer and vpc reachability analyzer for example they're based on propositional satisfiability and it's and its cousin called satisfiability modular theories it's a slight extension to it um and those they have they have pretty significant limitations about what you can do if you're willing to traditionally if you're willing to put a phd or a person with a phd at the award to run these tools then you could do tremendously more because because now they could guide the tool to do do really remarkable things and the challenge has been that there aren't that many people able to drive that don't have the background they're hard to manage you know just a whole bunch of reasons that it's that it's reasons reasons exactly uh and so that's where um you know long long we've been dreaming for a long time about these sort of i mean in today's lingo i would say it this way that language models that are trained over proofs right such that now the language models can run the automated reasoning tools or i might call them theorem Proverbs, Mechanical Theorem Proverbs.

10:47That was a dream we had. And we were thinking about how to do that, like training over all of our papers and archive and that kind of stuff. But what magically happened was that the mathematics community got really into the Lean Theorem Proverbs. Lean is written, was founded, and the main architect is Leo DeMora, who works at Amazon. So the world of mathematics embraced Lean when they're communicating with each other about their proofs, but also it allows people not at the top universities to learn the foundations of mathematics. But Lean caused people at scale to write down the foundations of mathematics, and that became really good training data for language models.

11:32And the language models began to get really good at running Lean. And so it's actually like DeepMind, DeepSeq, just a whole bunch of model providers are actually using Lean with reinforcement learning, for example, to build models. And for that reason, the models are usually pretty good at running these theorem proofers. And so that gives us now that like... Like it's a capability that you didn't have before. Yeah. Yeah. Yeah. So that, that's a really exciting, uh, sort of piece of the puzzle. So that's kind of changing how we're thinking about a lot of things right now. That's fascinating. It's an interesting, like I said, it's an interesting side effect of the general development of this sort of domain that it's sort of picked up this capability.

12:17Yeah. And I guess in the, in the idea of like the, there's the idea of like the world model, right? Like the, but if you, if you think Think about it like what that's giving you is more real data as opposed to human authored data, right? And the view is that the volume of human authored data is actually fairly limited and also flawed. The thing about a theorem prover is the data is not flawed and it actually gives you an infinite amount of data. There are an infinite number of statements you can make and prove or disprove with a theorem prover. And so that becomes incredible training data. And what we're seeing and what a lot of model providers are finding is that if you use these kinds of tools that you get transfer, they are more logical, they're more able to do good recipe design, they're more able to do the sorts of tasks that use the same part of your brain that you would use when you're trying to drive a mathematical proof through.

13:15so it's leaning on that that mental model if you like or approach to problem solving for other things yeah meaning it's better at the other things what we found is that basically the lean there are others is isabel this hall light actually all of the developed all of the founders of those tools all work at amazon these days but um but uh um the uh in the neuro in the world of neurosymbolic yeah or the world the world of where you like train models or you know reason reinforcement learning or there's various other ways of integrating these things that lean lean is kind of a lingua franca of of our world um and so that's that's pretty exciting that's really cool that's really cool and so let's let's you know we've been skirting around a little bit let's let's dump right in so obviously generative ai happened um it brought great utility and great capability and then folks started noticing that it would give you confidently incorrect answers aka hallucinations and so then there became the challenge of well i'm getting answers sometimes they're right sometimes they're wrong how do i know how do i approve or verify and so a lot of work's gone on in terms of applying automated reasoning checks through things like bedrock guardrails etc talk to us about how firstly how with the lens of automated reasoning we can think about the data or the answers produced by large language models and how we seek to actually verify truth and and incorrectness and hallucinations sure it's it's worth i think it's worth pointing out that that the two times that i mean we're both amazon employees so like right you'll appreciate this this uh and hopefully the listener can kind of understand what we're saying that amazon unlike other companies i've worked at has like all these mechanisms to drive connection to the customer and to me before i joined amazon that sounded kind of corny uh but what i've found is that that actually is a big driver for why automated reasoning is successful right you you in 2014-15 timeframe, it was the financial services institutions in New York.

15:32I happen to be in New York and London. So customers began, they had mathematical backgrounds, they had the need, and they began driving on it. And we're driving on it hard. And some very influential financial services institutions began to approach other financial services institutions and say to them, we need to support this and we need to help Amazon understand how valuable this work is that's brewing inside the company. And that same thing happened, actually, with Hallucination and Gen.AI. Interesting. So when Gen.AI happened, it was kind of, you know, the board members of most enterprise organizations' granddaughter showed them.

16:16Yeah. And then they began playing with it over the holiday break. And then by February, each C-suite leader of every enterprise organization needed to know what their gen ai plan was and so then they all you know uh diverted resources and then formed teams and went and did a bunch of stuff and and i began to get calls and again i'm in york city and london so like the financial services and a bunch of those sort of industries in in in in these areas up and down sixth avenue were calling me and so then i started i started ended up i was my my calendar was filling with meetings with customers and i was kind of hearing the same thing around but we won't be able to we can't trust this we can't use it like the prototypes are cool but like there were issues around privacy issues around sovereignty and then issues around incorrectness uh doodle hallucination and so those kind of became that a bunch of stuff that uh that scientists including myself began uh began tackling so the um so to to to kind of answer your question directly how i think about it um with with so we're sort of delving in the area of neurosymbolic so it's sort of the intersection so then with with much help from my friends you know who are more on the um statistical machine learning side uh jointly with them i've begun to appreciate that there's like multiple ways you can combine these tools so one is you can use automated reasoning to generate data that might train over and that would include reinforcement learning another way is to just allow the gna to do whatever it wants and then when it's done doing whatever it wants but whatever magic it's using and take that information and then prove or disprove its correctness and then another way is to integrate them more deeply so like in the inference step to provide hooks for logical reasoning.

18:08And then sort of a cousin to that is with, you know, agentic tools where you provide agentic access to the formal reasoning tools and then it's a multi-agent system to collaborate and then, you know, maybe the theorem prover provides a verification result together with a certificate that they audit to make sure that the theorem prover was really called and that your other agents are just hallucinating that answer. um and so that so those are those are some different ways and you're kind of seeing um and then and then when it comes to agentic ai then you have questions around well what are the agents doing and how do we know they're doing the right thing and then how do when we close them how do we know that we're doing the right thing and then can we plan over the compositions and so there's a whole there's a whole kind of uh rich area and and what we're seeing within amazon and you know i can't really speak to all the the products that'll that'll come out but i can't speak to automated using checks and bedrock guardrails is that there's different sort of points in that space and there's different solutions we can put together and we're basically sort of using all of them.

19:12Yeah, yeah. That's the thing. It's not one solution. It's lots of insertion points. Let's maybe unpack one accessible example, if I could put it that way for folks. So one of the examples we often talk about is like a generative AI solution that's doing mortgage approval type work. So it's assessing different stuff. The question is always, well, how do I know it's right? Now, mortgage approvals is good because there's lots and lots of rules, but the challenge is there's lots and lots of rules. So how does automated reasoning go from, there's a whole bunch of financial institution policies around lending to, is my answer correct?

19:47Like help us bridge that gap. Yeah. So, um, the,

19:56the statement i could make a statement that anyone who's worked in a formal reasoning for any length of time would agree with violently but people who haven't would be super puzzled by and that statement is that over 80 of the work is figuring out what it is you want to prove yeah start with my thing for any principle lives across the world on everything so we i'll give you some examples you know pre-gen ai right so uh so we launched im access analyzer right it's a tool automatically takes all your policies throws them in a big soup is able to reason at the semantic level about them is able to prove is able to prove properties and then im access analyzer walks you through an exercise to basically trick you into writing the specification right it is it is asking you a set of questions and basically building something that we're going to now prove of your system.

20:50And whenever your system diverts from that spec, then we're going to flag it to you. And then we're going to ask you that, okay. And then the spec evolves. But also, what are the semantics of the IAM policy language? Where are they precisely? And that turned out to be a multi-year effort. Wow. How high could it be? It turns out that no one really knew. And it turns out these days, if you ask questions hard enough, of AWS, what's going to happen is they're finally going to pull out someone from the IMXS analyzer team who has a background in mathematical logic who's then going to be answered because who owns it these days is those folks.

21:28And so we see that where increasingly people build on that semantics. Within AWS, we use that semantics for a lot of other purposes beyond IMXS analyzer. And sometimes when teams break the semantics, they're required to roll back the changes. So it actually becomes a very important um again another god round of customers is this is this is the semantics same thing with uh ec2 networking same story years years argument many meetings many people in the meeting many and so and and well i've worked on device drivers i've worked worked on biological systems i've worked on railways and so on it's always the same that you get three people three biologists uh who are working on models of leukemia or cancer you can't get agreement between the three of them right so So it actually turns out just the, what are the ground rules?

22:18What are the assumptions that we're making when we do this proof? And then what are the important properties? Like, is it all data at rest? Imagine like all data at rest must be encrypted. Sounds reasonable. Okay, well, what do you mean by encryption? Do you mean like a Caesar cipher? Oh, no, no, no. Caesar ciphers, that's totally insecure. Okay, but you just said all data at rest. You said encryption. Right, so encryption. So you didn't really mean, when you said encryption, you actually meant something else, right? And so that refinement loop takes a really long time. And so that's now what your customers who are going to try and do mortgage approvals or Family Medical Leave Act or questions about airline ticket returns policies or HR rules around leave of absence and stuff like that.

23:05And how does your stock interact with your leave of absence and so on? Turns out that it's really hard to work that out. It's really hard to figure out all the corner cases. It's hard to get agreement. And often, achieving agreement often becomes very controversial. Because when you're setting policy ahead of time, you're actually making an infinite set of decisions all at the same time. And people begin to find all the corner cases that they don't like the answers to. And so it's very hard to reach consensus. So we're basically taking, we're giving customers a big stick and helping them poke the wasp's nest of what is truth.

23:43And it's actually a very difficult challenge. Add to that the fact that we, because they don't understand, the average customer won't understand mathematical logic and we don't want to require that they do. We're basically having to maintain a, not a digital twin, like a logical twin. basically we we want to maintain a natural language representation of your rules together with the actual actual symbolic logical view and it might be that we want to take the logical view and communicate it to your natural language but it might be that we want to take your natural language and convert it into logic but i appreciate that you don't understand logic and then help you understand what's hidden in that logic um and what are all the weird corner cases and so there's i mean we can kind of zoom into all the techniques that we developed for automated reasoning checks, bro.

24:31But they're, they're super interesting. And then what we're finding, um, all around the company is, is that we're, we're, we're realizing that those are actually basic building blocks and we're reusing those, uh, a lot of those capabilities, um, in different parts of the company. And so, so it's, it's a pretty, it's a very, very exciting time right now. Let me say it that way. It is, it is. So, so if I'm, if I'm then a customer, let's, let's keep, let's keep picking away at this mortgage approval situation. So if I'm a customer, I'm using, you know, I'm using automated reasoning checks in guardrails, for example.

25:02So I can upload, I'll have documents, I'll have policies, et cetera. Is automated reasoning basically interpreting that and converting that into that mathematical model for me? Is it playing back maybe if it's detecting anomalies or, you know, as you say, you know, often these policies are built over time and actually have built in clashes with one another because they've never been applied to this. Like, what do you see in terms of that process from a customer standpoint? There are a lot of things we could do and probably we will end up doing. But at the first launch there, we're doing something more limited.

25:36So what we're doing is we're taking in PDFs and we are automatically synthesizing our first swing at what we believe the policy might be. In a formalism, it's called SMT, Satisfiability Modular Theories. so you have logical constants and you have axioms, basically. And then, so we axiomatize a representation of what we believe the document to be saying. We use generative AI to help us do that. So then the question is, whoa, whoa, whoa, like you're trying to mitigate hallucination and generative AI. And that same challenge is going to come up when we talk about inference time checks, so keep me honest to explain that to you too.

26:22right so we use generative ai to for help formulate and so then now now how do we help you get confidence that that it's right okay well what we can do is we can now we have a logical formula with propositional structure like ands and ors and nots and so on so we can walk that structure and find interesting corner cases embedded in the logical structure and then we can find examples in those, like we can find like the sort of convex holes to use a technical term, but the sort of different slices, if you will, of the formula. And then we can find exact witnesses of those formulae, and then we can translate them into natural language.

27:04And then we can say to you, hey, what would you think about this case? Thumbs up, thumbs down. And if you say thumbs down, then we're going to say, well, why not? And then you're going to give us a bit of text. and then we use that text to take another round of the prompting. And then we're using a technique from IMXS Analyzer. So basically, IMXS Analyzer is doing the same thing. We take all of your policies, and then we look at all of the weird corner cases that sort of are up to the parts of your policy. We basically take your policies, put them in a blender, and then get a whole bunch of interesting scenarios out of them, and then run them by you to say, what about this, what about this?

27:41but then we use some techniques from lattice theory to reduce the number of questions we're going to ask you. And it's something analogous to like green eggs and ham, like the, the Dr. Seuss story, right? Like if, if you've already said you don't need green eggs and ham, you don't need them with, in a car and on a bar, at a bar or whatever. Right. So we're able to like, we basically use some, those kinds of tricks to, to, to, um, reduce the overhead of that exercise, but it's not trivial, right? And so there's a bunch of science going on now about how to make that exercise easier and easier to understand.

28:18And then we can lock that down. And then there's a bunch of things you could do, right? So you could deploy this in production and then you could record your customer's Q &As, for example. Yes, yes. And then if you make a change to your policy later, you could go replay those with automated reasoning checks again to see how the rules change and how you give different answers. And then you can also query, you can also collect customer feedback on the questions, on the answers that they didn't think were right or you could audit them. And then you use that information to figure out which of the rules you actually have got wrong and sort of make an organizational level decision like do we want to change the rule?

29:00Do we not want to change the rule? And it's my hope and belief that in time that we will no longer use PDFs to decide policies, right? That the real source of truth will be mathematical logic and that people of the future probably won't understand mathematical logic per se, but they will have natural language... Abstraction. Yeah, exactly. Versions, representations of those, and that they because of um tricks that we have with generative ai that that that distance between those two things becomes um much smaller um i think i think that's what the interesting thing is because we want to get it down to that representation that benefits the ability to process but without the phd we have another trick that's that's very clever and then there's a whole bunch of science going on about how to do it even better but um i love i love byron there's this like the use of your phrase trick when when you're really what you're really saying is highly detailed incredibly complex amazing interesting mathematical work that's being done aka trick what we do is we so we we can do this both at the time when we're translating your documents but also at inference time right so imagine you are now an airline customer and you're asking a chat bot or or we could talk about how this translates to agent you know sops and agentic ai and so on but it's kind of the same question.

30:25So the customer is asking a question, how do we map that to mathematical logic at inference time, right? Because now we don't have the benefit of the like, oh, pump the brakes. Let's walk you through a bunch of examples, right? This is real time. Exactly. Grandma wants to know if she can change her ticket from her first class to a coach ticket. And it's a code share flight. And it's, you know, multiple airlines involved. And she wants to know now. And you can't say, we're going to like walk you through a semantics exercise so how do we do that well we we actually translate multiple times so you can take the same thing and you can use different language models you can use different settings of language models all kinds of things you do to basically exercise out the ambiguity in the statement so if the statement is unambiguous very often what we see is that we get semantically the same formula.

31:23They can be different syntactically, but they're equivalent semantically. And if there is ambiguity in the statement, we tend to get different formulae. And so what we can do now, so we basically imagine we get five translations, each from different language models or the same language model, but like just call different times. And then we use the theorem prover, you know, automated reasoning, to check that each of the pairs are equivalent. And if they are, then we're very confident we got the translation right. And if we don't, we get a counterexample, right? So one translation may assume it's first class.

32:00One of the translations may assume you've taken the flight and the other translation may assume you didn't take the flight. And so now we get to go back and we get to ask the customer or the customer's customer, right? Either the airline or the passenger. did you mean you've taken the flight or have you not taken the flight so we seek to solve for that ambiguity that has emerged as evident yeah and so that brings up all kinds of really interesting cognitive stuff which i'm now i'm talking to a lot to cognitive psychologists and so on and so there's a whole thing about theory of mind and around how people build mental models about what each other understands and they convey information in in ways that's efficient but but leverages the shared mental model.

32:43And so basically what's happening is that inference time, we are trying to build literally a logical representation of the mental model that the customer has or the customer's customer quickly and then to such that we can now reason about that formally and then provide evidence as to why the answer is correct. So that's turned out to be very interesting work. And it's interesting if I sort of just as we come towards the end of the episode here, I'm thinking that throughout what we've been talking about, a lot of it has come down to bringing the capabilities and the sophistication of automated reasoning, the complexity, if you like, to a level that can be accessible to non-specialist people, that can be accessed by systems, etc.

33:26There's kind of this ability to introduce it to more use cases, because as you said at the start, you don't need the PhD necessarily sitting there all the time. This sounds like it's likely to actually create a kind of phase of hyper growth in the use of this technology and the advancement of this. So this is really interesting to me that suddenly it's just going to explode. So here's the fascinating bit, right? Your SMT or SAT solvers, they're MP complete typically. So that's intractably large, right? That's the famous, you know, the hard problems. But those are the easy ones. By our... That's breakfast.

34:02MP complete is practically boring because for us, the hard problems are the undecidable ones. right? So there are, practically speaking, whether or not it's NP-complete or undecidable, what that really means is that the tools will from time to time not be able to answer the question. They can answer, they can be correct, they can say the theorem is not true or the theorem is true, and you can rely on those answers, but sometimes they will just either never come back with an answer or they'll just come back and say, I don't know. So that is a natural consequence of NP-complete or undecidable problems.

34:37That's a fundamental computer science, you know, intro to the theory of computer science, one-on-one kind of idea. Yeah, it's there, yeah. And the challenge is that it's fundamental. So the only way to deal with it is to get as close as you can to the customer to appreciate the type of problem they're asking because you're trying to statistically cause those cases. You want those cases to be so few that the customer still benefits from using the tool. And so it's a very interesting, it's a good UX and design and a customer connection and formal reasoning are comorbid. They live together. They live together.

35:28Yeah. It's true. And it's interesting. I think more folks are getting familiar with that concept somewhat unconsciously Because if you think about folks using these tools in their daily lives, most people know that if you do a broad one-shot statement to your chatbot of choice, you're going to get a pretty questionable answer. Versus if you take the time to think about your domain, think about your scope, think about what you want the tool to do, you'll typically get a much higher quality answer. There's kind of speaking that same thing of scope down and then suddenly good stuff happens. It is amazing to watch our society discover how hard it is to get to truth in complex domains.