Vervulbaarheid en modelgeneratie in oneindige ruimtes

Het uiteindelijke doel van declaratieve problemen op te lossen is voor de menselijke deskundige informatie over een probleem domein in een logica te vertegenwoordigen en om problemen op te lossen en uit te voeren taken door het uitvoeren van generieke, domein onafhankelijke gevolgtrekking motoren op deze voorstellingen. Dit doel wordt nagestreefd in verschillende declaratieve en formele programmering paradigma's (constraint programming, operationeel onderzoek, logisch programmeren, SAT en SMT). Het resulteert vaak in een spectaculaire verbetering van de ontwikkeling van de tijd, code grootte en de oplossing kwaliteit met acceptabele prestaties. Met de FO (.) - Kennisbank Systeem, ontwikkelden we een van de rijkste declaratieve talen-to-date en gecombineerd met meerdere vormen van gevolgtrekking. Echter, het systeem heeft slechts een eindig domein solver; Het is niet geschikt voor computers met oneindige types zoals lijsten, strings, bomen, onbegrensde aantallen, sets, enz. Deze beperking is momenteel onbetaalbaar. Traditioneel logica en functioneel programmeren kan behandelen onbegrensde domeinen, maar geeft slechts een enkele vorm van inferentie. Ons doel is om het beste van beide werelden te krijgen door uitbreiding van de FO (.) Modellering taal met de infinitary kenmerken van de laatstgenoemde talen (complexe datastructuren, hogere orde bouwt en modulariteit ondersteuning), en het ontwikkelen van nieuwe afleidingsalgoritmen voor de uitgebreide taal. Dit vereist het ontwerp van een nieuwe taal, nieuwe inferentiemethoden en de uitvoering ervan. Als gevolg hiervan wordt de klasse van praktische problemen die bevredigend kunnen worden aangepakt door het modelleren sterk uitgebreid.